| (* Copyright (c) 2017, the Dart project authors. Please see the AUTHORS file |
| * for details. All rights reserved. Use of this source code is governed by a |
| * BSD-style license that can be found in the LICENSE file. *) |
| |
| |
| Require Import Coq.Lists.List. |
| Require Import Common. |
| Require Import Syntax. |
| Require Import ObjectModel. |
| |
| |
| (** Placeholder for a mapping from function node ids to function nodes. At |
| some point the mapping should be defined in the syntax module along with its |
| well-formedness definitions. *) |
| Definition func_env : Type := NatMap.t function_node. |
| |
| |
| Section OperationalSemantics. |
| |
| |
| (** This instance of [class_env] is referred in many properties in the section |
| for the operational semantics. One may think about [CE] as a "global" class |
| environment for the program. *) |
| Variable CE : class_env. |
| |
| |
| (** The "global" environment of function nodes for the program. *) |
| Variable FE : func_env. |
| |
| (** Placeholder for one of the well-formedness properties of the program. At |
| some point a property like this one (or another property that will allow this |
| property to be established) should be defined in the syntax module. *) |
| Hypothesis program_wf: |
| forall class_id intf proc_desc, |
| NatMap.MapsTo class_id intf CE -> |
| List.In proc_desc (procedures intf) -> |
| NatMap.In (pr_ref proc_desc) FE. |
| |
| |
| (** [runtime_value] represents the runtime values used in the abstract machine |
| during program execution. The values are typed and have some relation to |
| syntactic types and internal representation of their interfaces. Currently a |
| runtime value doesn't have a state, it only has a type. It should have a |
| state when a broader subset of Kernel is formalized. *) |
| Record runtime_value := mk_runtime_value { |
| |
| (** In the currently formalized subset of Kernel any runtime type can be |
| represented by a syntactic description that is not necessarily defined |
| in the program. In all cases we assume how such type could be potentially |
| given using the syntax of the current Kernel subset. |
| |
| Null is currently modelled using None as the value of [syntactic_type]. |
| It may change in future once [dart_type] includes a constructor for Null |
| or Bottom. *) |
| syntactic_type : option dart_type; |
| }. |
| |
| |
| (** [value_of_type] defines the meaning of statement "the runtime value has the |
| given interface and the given syntactic type". *) |
| Inductive value_of_type : |
| runtime_value -> interface -> option dart_type -> Prop := |
| |
| (** If the syntactic type of the runtime value is an interface type, then the |
| corresponding interface should be in the global class environment. *) |
| | RFS_Interface_Type : |
| forall (val : runtime_value) (intf : interface) (type : dart_type) |
| (class_id : nat), |
| type = DT_Interface_Type (Interface_Type class_id) -> |
| NatMap.find class_id CE = Some intf -> |
| (syntactic_type val) = Some type -> |
| value_of_type val intf (Some type) |
| |
| (** If the syntactic type of the runtime value is a function type, then the |
| corresponding interface may or may not be in the global class environment, |
| but should have a particular shape. *) |
| | RFS_Function_Type : |
| forall (val : runtime_value) (intf : interface) (type : dart_type) |
| (par_type ret_type : dart_type) |
| (proc : procedure_desc) (proc_rest : list procedure_desc), |
| type = DT_Function_Type (Function_Type par_type ret_type) -> |
| List.length (procedures intf) = 1%nat -> |
| (procedures intf) = List.cons proc proc_rest -> |
| ((pr_name proc) = "call")%string -> |
| (pr_type proc) = Function_Type par_type ret_type -> |
| NatMap.In (pr_ref proc) FE -> |
| (syntactic_type val) = Some type -> |
| value_of_type val intf (Some type) |
| |
| | RFS_Null_Type : |
| forall (val : runtime_value) (intf : interface), |
| (procedures intf) = nil -> |
| (syntactic_type val) = None -> |
| value_of_type val intf None. |
| |
| |
| (** The environment that is used by the abstract machine to map the currently |
| visible set of variables to their runtime values is represented as a list of |
| pairs. *) |
| Record environment_entry := mk_environment_entry { |
| variable_id : nat; |
| value : runtime_value; |
| }. |
| |
| Definition environment := list environment_entry. |
| |
| Definition env_get : nat -> environment -> option environment_entry := |
| fun var_id env => |
| List.find (fun entry => Nat.eqb var_id (variable_id entry)) env. |
| |
| Definition env_extend : nat -> runtime_value -> environment -> environment := |
| fun var_id val env => (mk_environment_entry var_id val) :: env. |
| |
| Definition empty_env : environment := nil. |
| |
| (* TODO(dmitryas): Add some hypotheses about well-formedness of an environment |
| w.r.t. to other components. *) |
| |
| |
| (** TODO(dmitryas): Write descriptive comments. *) |
| Inductive expression_continuation : Set := |
| |
| (** The constructor receives the following parameters: |
| |
| - an [environment] |
| - an [expression_continuation] |
| - a [statement_continuation] *) |
| | Expression_Ek : |
| environment |
| -> expression_continuation |
| -> statement_continuation |
| -> expression_continuation |
| |
| (** The constructor receives the following parameters: |
| |
| - a [string] |
| - an [expression] |
| - an [environment] |
| - an [expression_continuation] *) |
| | Method_Invocation_Ek : |
| string |
| -> expression |
| -> environment |
| -> expression_continuation |
| -> expression_continuation |
| |
| (** The constructor receives the following parameters: |
| |
| - a [runtime_value] |
| - a [string] |
| - an [environment] |
| - an [expression_continuation] *) |
| | Invocation_Ek : |
| runtime_value |
| -> string |
| -> environment |
| -> expression_continuation |
| -> expression_continuation |
| |
| (** The constructor receives the following parameters: |
| |
| - a [string] |
| - an [expression_continuation] *) |
| | Property_Get_Ek : |
| string |
| -> expression_continuation |
| -> expression_continuation |
| |
| (** TODO(dmitryas): Write descriptive comments. *) |
| with statement_continuation : Set := |
| |
| (** The constructor receives the following parameters: |
| |
| - an [expression_continuation] |
| - a [runtime_value] *) |
| | Exit_Sk : |
| expression_continuation |
| -> runtime_value |
| -> statement_continuation |
| |
| (** The constructor receives the following parameters: |
| |
| - a list of [statement]s |
| - an [environment] |
| - an [expression_continuation] |
| - a [statement_continuation] *) |
| | Block_Sk : |
| list statement |
| -> environment |
| -> expression_continuation |
| -> statement_continuation |
| -> statement_continuation. |
| |
| |
| (** [configuration] represents configurations of the CESK abstract machine that |
| is used for defining the operational semantics. A transition of the machine |
| represents a small step of the small-step operational semantics. There are |
| the following types of configurations: |
| |
| - [Eval_Configuration] -- encapsulates a syntactic expression and an |
| expression continuation. After evaluation of the expression the resulting |
| value is passed to the expression configuration. |
| - [Exec_Configuration] -- encapsulates a syntactic statement. Represents the |
| execution of the statement. |
| - [Value_Passing_Configuration] -- encapsulates a value and an expression |
| continuation. The value is passed to the expression continuation. |
| - [Forward_Configuration] -- encapsulates a statement continuation. |
| The execution of the program proceeds to the associated statement. *) |
| Inductive configuration : Set := |
| |
| (** [Eval_Configuration] represents the beginning of an expression |
| evaluation. The constructor receives the following parameters: |
| |
| - an [expression] -- the expression to be evaluated; |
| - an [environment] -- the mapping from variables to values that is to be |
| used during the expression evaluation; |
| - an [expression_continuation] -- the continuation that will receive the |
| value of the expression after its evaluation. *) |
| | Eval_Configuration : |
| expression |
| -> environment |
| -> expression_continuation |
| -> configuration |
| |
| (** [Exec_Configuration] represents the beginning of a statement execution. |
| The constructor receives the following parameters: |
| |
| - a [statement] -- the statement to be executed; |
| - an [environment] -- the mapping from variables to values that is to be |
| used during the statement execution; |
| - an [expression_continuation] -- in case the executed statement returns a |
| value, this continuation will receive this value; |
| - a [statement_continuation] -- in case the executed statement doesn't |
| return a value, this continuation represents the rest of the program |
| execution. *) |
| | Exec_Configuration : |
| statement |
| -> environment |
| -> expression_continuation |
| -> statement_continuation |
| -> configuration |
| |
| (** [Value_Passing_Configuration] represents the end of an expression |
| evaluation. The constructor receives the following parameters: |
| |
| - an [expression_continuation] -- the continuation that receives the value |
| which is the result of the expression evaluation; |
| - a [value] -- the result of the expression evaluation. *) |
| | Value_Passing_Configuration : |
| expression_continuation |
| -> runtime_value |
| -> configuration |
| |
| (** [Forward_Configuration] represents the rest of the program execution. |
| The constructor receives the following parameters: |
| |
| - a [statement_continuation] -- represents the rest of the program |
| execution; |
| - an [environment] -- the mapping from variables to values that is to be |
| used during the execution of the rest of the program. *) |
| | Forward_Configuration : |
| statement_continuation |
| -> environment |
| -> configuration. |
| |
| |
| (** Represents steps (a.k.a. transitions) of the abstract machine. *) |
| Inductive step : configuration -> configuration -> Prop := |
| |
| (** <Block(stmt :: stmts), ρ, κE, κS>exec ==> |
| <stmt, ρ, κE, BlockSK(stmts, ρ, κE, κS)>exec *) |
| | Exec_Block : |
| forall stmt stmts env ret_cont next_cont, |
| step (Exec_Configuration |
| (S_Block (Block (stmt :: stmts))) env ret_cont next_cont) |
| (Exec_Configuration |
| stmt env ret_cont (Block_Sk stmts env ret_cont next_cont)) |
| |
| (** <Block(#[]#), ρ, κE, κS>exec ==> <κS, ρ>forward *) |
| | Exec_Block_Empty : |
| forall env ret_cont next_cont, |
| step (Exec_Configuration (S_Block (Block nil)) env ret_cont next_cont) |
| (Forward_Configuration next_cont env) |
| |
| (** <BlockSK(stmt :: stmts, ρ, κE, κS), ρ'>forward ==> |
| <stmt, ρ', κE, BlockSK(stmts, ρ, κE, κS)>exec *) |
| | Forward_Block_Sk : |
| forall stmt stmts env ret_cont next_cont env', |
| step (Forward_Configuration |
| (Block_Sk (stmt :: stmts) env ret_cont next_cont) env') |
| (Exec_Configuration |
| stmt env' ret_cont (Block_Sk stmts env ret_cont next_cont)) |
| |
| (** <BlockSK(#[]#, ρ, κE, κS), ρ'>forward ==> <κS, ρ>forward *) |
| | Forward_Block_Sk_Empty : |
| forall env ret_cont next_cont env', |
| step (Forward_Configuration (Block_Sk nil env ret_cont next_cont) env') |
| (Forward_Configuration next_cont env) |
| |
| (** <ExpressionStatement(expr), ρ, κE, κS>exec ==> |
| <expr, ρ, ExpressionEK(ρ, κE, κS)>eval *) |
| | Exec_Expression_Statement : |
| forall expr env ret_cont next_cont, |
| step (Exec_Configuration |
| (S_Expression_Statement (Expression_Statement expr)) |
| env ret_cont next_cont) |
| (Eval_Configuration expr env (Expression_Ek env ret_cont next_cont)) |
| |
| (** <ReturnStatement(expr), ρ, κE, κS>exec ==> <expr, ρ, κE>eval *) |
| | Exec_Return_Statement : |
| forall expr env ret_cont next_cont, |
| step (Exec_Configuration |
| (S_Return_Statement (Return_Statement expr)) |
| env ret_cont next_cont) |
| (Eval_Configuration expr env ret_cont) |
| |
| (** <VariableGet(var), ρ, κE>eval ==> <κE, ρ(var)>pass *) |
| | Eval_Variable_Get : |
| forall var_id env cont entry, |
| env_get var_id env = Some entry -> |
| step (Eval_Configuration (E_Variable_Get (Variable_Get var_id)) env cont) |
| (Value_Passing_Configuration cont (value entry)) |
| |
| (** <MethodInvocation(rcvr, name, arg), ρ, κE>eval ==> |
| <rcvr, ρ, MethodInvocationEK(name, arg, ρ, κE)>eval *) |
| | Eval_Method_Invocation : |
| (* TODO(dmitryas): Remove [ref] after interfaceTargetReference is removed |
| from constructor [Method_Invocation]. *) |
| forall rcvr name arg env cont ref, |
| step (Eval_Configuration |
| (E_Invocation_Expression (IE_Method_Invocation |
| (Method_Invocation rcvr (Name name) (Arguments arg) ref))) |
| env cont) |
| (Eval_Configuration rcvr env |
| (Method_Invocation_Ek name arg env cont)) |
| |
| (** <MethodInvocationEK(name, arg, ρ, κE), rcvrVal)pass ==> |
| <arg, ρ, InvocationEK(rcvrVal, name, ρ, κE)>eval *) |
| | Pass_Method_Invocation_Ek : |
| forall name arg env cont val, |
| step (Value_Passing_Configuration |
| (Method_Invocation_Ek name arg env cont) val) |
| (Eval_Configuration arg env (Invocation_Ek val name env cont)) |
| |
| (** <InvocationEK(rcvrVal, name, ρ, κE), argVal>pass ==> |
| <block, ρ', κE, κS>exec, |
| where ρ' = ρ0#[#this = rcvrVal#][#arg(f) = argVal#]#, |
| block = body(f), |
| κS = ExitSK(κE, nullVal), |
| f = methods(class(rcvrVal))(name), |
| ρ0 -- empty environment *) |
| | Pass_Invocation_Ek : |
| forall rcvr_val name env ret_cont arg_val body env' next_cont |
| intf type proc_desc proc var_id var_type var_init ret_type null_val, |
| (* TODO(dmitryas): Add the mapping: this -> rcvr_val to env'. *) |
| value_of_type rcvr_val intf type -> |
| List.In proc_desc (procedures intf) -> |
| NatMap.MapsTo (pr_ref proc_desc) proc FE -> |
| proc = Function_Node (Variable_Declaration var_id var_type var_init) |
| ret_type body -> |
| env' = env_extend var_id arg_val empty_env -> |
| next_cont = Exit_Sk ret_cont null_val -> |
| value_of_type null_val (mk_interface nil) None -> |
| step (Value_Passing_Configuration |
| (Invocation_Ek rcvr_val name env ret_cont) arg_val) |
| (Exec_Configuration body env' ret_cont next_cont) |
| |
| (** <PropertyGet(rcvr, name), ρ, κE>eval ==> |
| <rcvr, ρ, PropertyGetEK(name, κE)>eval *) |
| | Eval_Property_Get : |
| forall rcvr name env cont, |
| step (Eval_Configuration (E_Property_Get (Property_Get rcvr (Name name))) |
| env cont) |
| (Eval_Configuration rcvr env (Property_Get_Ek name cont)) |
| |
| (** <PropertyGetEK(name, κE), rcvrVal)pass ==> <κE, f>pass, |
| where f = methods(class(rcvrVal))(name) *) |
| | Pass_Property_Get_Ek : |
| forall name cont rcvr_val rcvr_intf rcvr_type func_val proc_desc, |
| value_of_type rcvr_val rcvr_intf rcvr_type -> |
| List.In proc_desc (procedures rcvr_intf) -> |
| (pr_name proc_desc) = name -> |
| value_of_type |
| func_val |
| (mk_interface (proc_desc :: nil)) |
| (Some (DT_Function_Type (pr_type proc_desc))) -> |
| step (Value_Passing_Configuration (Property_Get_Ek name cont) rcvr_val) |
| (Value_Passing_Configuration cont func_val) |
| |
| (** <ExitSK(κE, val), ρ>forward ==> <κE, val>pass *) |
| | Forward_Exit_Sk : |
| forall cont val env, |
| step (Forward_Configuration (Exit_Sk cont val) env) |
| (Value_Passing_Configuration cont val) |
| |
| (** <ConstructorInvocation(cls), ρ, κE>eval ==> <κE, newVal>pass, |
| where newVal = new runtime value of syntactic type cls *) |
| | Eval_Constructor_Invocation : |
| forall env cont new_val intf type proc_desc, |
| value_of_type new_val intf type -> |
| List.In proc_desc (procedures intf) -> |
| step (Eval_Configuration |
| (E_Invocation_Expression (IE_Constructor_Invocation |
| (Constructor_Invocation (pr_ref proc_desc)))) |
| env cont) |
| (Value_Passing_Configuration cont new_val). |
| |
| |
| End OperationalSemantics. |