eval
Zhi Zhang Department of Computer and Information Sciences Kansas State University zhangzhi@ksu.edu
Require Export list_util.
Require Export values.
Require Export environment.
Require Export symboltable.
Require Export CpdtTactics.
Module Entry_Value_Stored <: ENTRY.
Definition T := value.
End Entry_Value_Stored.
Module STACK := STORE(Entry_Value_Stored).
Import STACK.
Run-Time Check Evaluation
Overflow Check
check whether a value falls into the bound of basic integer type
Inductive overflowCheck: Z -> Ret value -> Prop :=
| OverflowCheck_Fail: forall v,
in_bound v int32_bound false ->
overflowCheck v (RTE OverflowError)
| OverflowCheck_OK: forall v,
in_bound v int32_bound true ->
overflowCheck v (OK (Int v)).
| OverflowCheck_Fail: forall v,
in_bound v int32_bound false ->
overflowCheck v (RTE OverflowError)
| OverflowCheck_OK: forall v,
in_bound v int32_bound true ->
overflowCheck v (OK (Int v)).
Inductive divCheck: binary_operator -> Z -> Z -> Ret value -> Prop :=
| DivCheck_RTE: forall op dividend divisor,
op = Divide \/ op = Modulus ->
(Zeq_bool divisor 0) = true ->
divCheck op dividend divisor (RTE DivByZero)
| DivCheck_D: forall dividend divisor v,
(Zeq_bool divisor 0) = false ->
Math.div (Int dividend) (Int divisor) = Some v ->
divCheck Divide dividend divisor (OK v)
| DivCheck_M: forall dividend divisor v,
(Zeq_bool divisor 0) = false ->
Math.mod' (Int dividend) (Int divisor) = Some v ->
divCheck Modulus dividend divisor (OK v).
| DivCheck_RTE: forall op dividend divisor,
op = Divide \/ op = Modulus ->
(Zeq_bool divisor 0) = true ->
divCheck op dividend divisor (RTE DivByZero)
| DivCheck_D: forall dividend divisor v,
(Zeq_bool divisor 0) = false ->
Math.div (Int dividend) (Int divisor) = Some v ->
divCheck Divide dividend divisor (OK v)
| DivCheck_M: forall dividend divisor v,
(Zeq_bool divisor 0) = false ->
Math.mod' (Int dividend) (Int divisor) = Some v ->
divCheck Modulus dividend divisor (OK v).
Inductive rangeCheck: Z -> Z -> Z -> Ret value -> Prop :=
| RangeCheck_Fail: forall v l u,
in_bound v (Interval l u) false ->
rangeCheck v l u (RTE RangeError)
| RangeCheck_OK: forall v l u,
in_bound v (Interval l u) true ->
rangeCheck v l u (OK (Int v)).
| RangeCheck_Fail: forall v l u,
in_bound v (Interval l u) false ->
rangeCheck v l u (RTE RangeError)
| RangeCheck_OK: forall v l u,
in_bound v (Interval l u) true ->
rangeCheck v l u (OK (Int v)).
Inductive do_run_time_check_on_binop: binary_operator -> value -> value -> Ret value -> Prop :=
| DoCheckOnBinops: forall op v1 v2 v v',
op = Plus \/ op = Minus \/ op = Multiply ->
Math.binary_operation op v1 v2 = Some (Int v) ->
overflowCheck v v' ->
do_run_time_check_on_binop op v1 v2 v'
| DoCheckOnDivide_RTE: forall v1 v2,
divCheck Divide v1 v2 (RTE DivByZero) ->
do_run_time_check_on_binop Divide (Int v1) (Int v2) (RTE DivByZero)
| DoCheckOnDivide: forall v1 v2 v v',
divCheck Divide v1 v2 (OK (Int v)) ->
overflowCheck v v' ->
do_run_time_check_on_binop Divide (Int v1) (Int v2) v'
| DoCheckOnModulus: forall v1 v2 v',
divCheck Modulus v1 v2 v' ->
do_run_time_check_on_binop Modulus (Int v1) (Int v2) v'
| DoCheckOnBinOp_Others: forall op v1 v2 v,
op <> Plus ->
op <> Minus ->
op <> Multiply ->
op <> Divide ->
op <> Modulus ->
Math.binary_operation op v1 v2 = Some v ->
do_run_time_check_on_binop op v1 v2 (OK v).
| DoCheckOnBinops: forall op v1 v2 v v',
op = Plus \/ op = Minus \/ op = Multiply ->
Math.binary_operation op v1 v2 = Some (Int v) ->
overflowCheck v v' ->
do_run_time_check_on_binop op v1 v2 v'
| DoCheckOnDivide_RTE: forall v1 v2,
divCheck Divide v1 v2 (RTE DivByZero) ->
do_run_time_check_on_binop Divide (Int v1) (Int v2) (RTE DivByZero)
| DoCheckOnDivide: forall v1 v2 v v',
divCheck Divide v1 v2 (OK (Int v)) ->
overflowCheck v v' ->
do_run_time_check_on_binop Divide (Int v1) (Int v2) v'
| DoCheckOnModulus: forall v1 v2 v',
divCheck Modulus v1 v2 v' ->
do_run_time_check_on_binop Modulus (Int v1) (Int v2) v'
| DoCheckOnBinOp_Others: forall op v1 v2 v,
op <> Plus ->
op <> Minus ->
op <> Multiply ->
op <> Divide ->
op <> Modulus ->
Math.binary_operation op v1 v2 = Some v ->
do_run_time_check_on_binop op v1 v2 (OK v).
Inductive do_run_time_check_on_unop: unary_operator -> value -> Ret value -> Prop :=
| DoCheckOnUnary_Minus: forall v v' v'',
Math.unary_minus v = Some (Int v') ->
overflowCheck v' v'' ->
do_run_time_check_on_unop Unary_Minus v v''
| DoCheckOnUnOp_Others: forall op v v',
op <> Unary_Minus ->
Math.unary_operation op v = Some v' ->
do_run_time_check_on_unop op v (OK v').
| DoCheckOnUnary_Minus: forall v v' v'',
Math.unary_minus v = Some (Int v') ->
overflowCheck v' v'' ->
do_run_time_check_on_unop Unary_Minus v v''
| DoCheckOnUnOp_Others: forall op v v',
op <> Unary_Minus ->
Math.unary_operation op v = Some v' ->
do_run_time_check_on_unop op v (OK v').
given a record value r, get the value of its field f
Function record_select (r: list (idnum * value)) (f: idnum): option value :=
match r with
| (f1, v1) :: r1 =>
if beq_nat f1 f then
Some v1
else
record_select r1 f
| nil => None
end.
match r with
| (f1, v1) :: r1 =>
if beq_nat f1 f then
Some v1
else
record_select r1 f
| nil => None
end.
given an array value a, get its component value indexed by i
Function array_select (a: list (arrindex * value)) (i: Z): option value :=
match a with
| (i0, v0) :: a1 =>
if Zeq_bool i0 i then
Some v0
else
array_select a1 i
| nil => None
end.
match a with
| (i0, v0) :: a1 =>
if Zeq_bool i0 i then
Some v0
else
array_select a1 i
| nil => None
end.
Inductive evalLiteral: literal -> Ret value -> Prop :=
| EvalLiteral_Bool: forall v,
evalLiteral (Boolean_Literal v) (OK (Bool v))
| EvalLiteral_Int: forall v v',
overflowCheck v v' ->
evalLiteral (Integer_Literal v) v'.
| EvalLiteral_Bool: forall v,
evalLiteral (Boolean_Literal v) (OK (Bool v))
| EvalLiteral_Int: forall v v',
overflowCheck v v' ->
evalLiteral (Integer_Literal v) v'.
Expression Evaluation
Inductive evalExp: symTab -> state -> exp -> Ret value -> Prop :=
| EvalLiteral: forall l v st s n,
evalLiteral l v ->
evalExp st s (Literal n l) v
| EvalName: forall s nm v st n,
evalName st s nm v ->
evalExp st s (Name n nm) v
| EvalBinOpE1_RTE: forall st s e1 msg n op e2,
evalExp st s e1 (RTE msg) ->
evalExp st s (BinOp n op e1 e2) (RTE msg)
| EvalBinOpE2_RTE: forall st s e1 v1 e2 msg n op,
evalExp st s e1 (OK v1) ->
evalExp st s e2 (RTE msg) ->
evalExp st s (BinOp n op e1 e2) (RTE msg)
| EvalBinOp: forall st s e1 v1 e2 v2 op v n,
evalExp st s e1 (OK v1) ->
evalExp st s e2 (OK v2) ->
do_run_time_check_on_binop op v1 v2 v ->
evalExp st s (BinOp n op e1 e2) v
| EvalUnOp_RTE: forall st s e msg n op,
evalExp st s e (RTE msg) ->
evalExp st s (UnOp n op e) (RTE msg)
| EvalUnOp: forall st s e v op v' n,
evalExp st s e (OK v) ->
do_run_time_check_on_unop op v v' ->
evalExp st s (UnOp n op e) v'
with evalName: symTab -> state -> name -> Ret value -> Prop :=
| EvalIdentifier: forall x s v st n,
fetchG x s = Some v ->
evalName st s (Identifier n x) (OK v)
| EvalIndexedComponentX_RTE: forall st s x msg n e,
evalName st s x (RTE msg) ->
evalName st s (IndexedComponent n x e) (RTE msg)
| EvalIndexedComponentE_RTE: forall st s x a e msg n,
evalName st s x (OK (ArrayV a)) ->
evalExp st s e (RTE msg) ->
evalName st s (IndexedComponent n x e) (RTE msg)
| EvalIndexedComponent_Range_RTE: forall st s x a e i t l u n,
evalName st s x (OK (ArrayV a)) ->
evalExp st s e (OK (Int i)) ->
fetch_exp_type (name_astnum x) st = Some (Array_Type t) ->
extract_array_index_range st t (Range l u) ->
rangeCheck i l u (RTE RangeError) ->
evalName st s (IndexedComponent n x e) (RTE RangeError)
| EvalIndexedComponent: forall st s x a e i t l u v n,
evalName st s x (OK (ArrayV a)) ->
evalExp st s e (OK (Int i)) ->
fetch_exp_type (name_astnum x) st = Some (Array_Type t) ->
extract_array_index_range st t (Range l u) ->
rangeCheck i l u (OK (Int i)) ->
array_select a i = Some v ->
evalName st s (IndexedComponent n x e) (OK v)
| EvalSelectedComponentX_RTE: forall st s x msg n f,
evalName st s x (RTE msg) ->
evalName st s (SelectedComponent n x f) (RTE msg)
| EvalSelectedComponent: forall st s x r f v n,
evalName st s x (OK (RecordV r)) ->
record_select r f = Some v ->
evalName st s (SelectedComponent n x f) (OK v).
| EvalIdentifier: forall x s v st n,
fetchG x s = Some v ->
evalName st s (Identifier n x) (OK v)
| EvalIndexedComponentX_RTE: forall st s x msg n e,
evalName st s x (RTE msg) ->
evalName st s (IndexedComponent n x e) (RTE msg)
| EvalIndexedComponentE_RTE: forall st s x a e msg n,
evalName st s x (OK (ArrayV a)) ->
evalExp st s e (RTE msg) ->
evalName st s (IndexedComponent n x e) (RTE msg)
| EvalIndexedComponent_Range_RTE: forall st s x a e i t l u n,
evalName st s x (OK (ArrayV a)) ->
evalExp st s e (OK (Int i)) ->
fetch_exp_type (name_astnum x) st = Some (Array_Type t) ->
extract_array_index_range st t (Range l u) ->
rangeCheck i l u (RTE RangeError) ->
evalName st s (IndexedComponent n x e) (RTE RangeError)
| EvalIndexedComponent: forall st s x a e i t l u v n,
evalName st s x (OK (ArrayV a)) ->
evalExp st s e (OK (Int i)) ->
fetch_exp_type (name_astnum x) st = Some (Array_Type t) ->
extract_array_index_range st t (Range l u) ->
rangeCheck i l u (OK (Int i)) ->
array_select a i = Some v ->
evalName st s (IndexedComponent n x e) (OK v)
| EvalSelectedComponentX_RTE: forall st s x msg n f,
evalName st s x (RTE msg) ->
evalName st s (SelectedComponent n x f) (RTE msg)
| EvalSelectedComponent: forall st s x r f v n,
evalName st s x (OK (RecordV r)) ->
record_select r f = Some v ->
evalName st s (SelectedComponent n x f) (OK v).
Declaration Evaluation
Inductive semantic of declarations eval_decl st s sto decl rsto means that rsto is the frame to be pushed on s after evaluating decl, sto is used as an accumulator for building the frame;Inductive evalDecl: symTab -> state -> frame -> decl -> Ret frame -> Prop :=
| EvalDecl_Null: forall st s f,
evalDecl st s f NullDecl (OK f)
| EvalDecl_Type: forall st s f n t,
evalDecl st s f (TypeDecl n t) (OK f)
| EvalDecl_Var_None: forall d st s f n,
d.(initialization_exp) = None ->
evalDecl st s f (ObjDecl n d) (OK (push f d.(object_name) Undefined))
| EvalDecl_Var_RTE: forall d e st f s msg n,
d.(initialization_exp) = Some e ->
evalExp st (f :: s) e (RTE msg) ->
evalDecl st s f (ObjDecl n d) (RTE msg)
| EvalDecl_Var: forall d e st f s v n,
d.(initialization_exp) = Some e ->
evalExp st (f :: s) e (OK v) ->
v <> Undefined ->
is_range_constrainted_type (d.(object_nominal_subtype)) = false ->
evalDecl st s f (ObjDecl n d) (OK (push f d.(object_name) v))
| EvalDecl_Var_Range_RTE: forall d e st f s v l u n,
d.(initialization_exp) = Some e ->
evalExp st (f :: s) e (OK (Int v)) ->
extract_subtype_range st (d.(object_nominal_subtype)) (Range l u) ->
rangeCheck v l u (RTE RangeError) ->
evalDecl st s f (ObjDecl n d) (RTE RangeError)
| EvalDecl_Var_Range: forall d e st f s v l u n,
d.(initialization_exp) = Some e ->
evalExp st (f :: s) e (OK (Int v)) ->
extract_subtype_range st (d.(object_nominal_subtype)) (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
evalDecl st s f (ObjDecl n d) (OK (push f d.(object_name) (Int v)))
| EvalDecl_Proc: forall st s f n p,
evalDecl st s f (ProcBodyDecl n p) (OK f)
| EvalDecl_Seq_RTE: forall st s f d1 msg n d2,
evalDecl st s f d1 (RTE msg) ->
evalDecl st s f (SeqDecl n d1 d2) (RTE msg)
| EvalDecl_Seq: forall st s f d1 f' d2 f'' n,
evalDecl st s f d1 (OK f') ->
evalDecl st s f' d2 f'' ->
evalDecl st s f (SeqDecl n d1 d2) f''.
update the ith element of array a by value v: ai := v
Function updateIndexedComp (a: list (arrindex * value)) (i: arrindex) (v: value): list (arrindex * value) :=
match a with
| (i0, v0)::a1 =>
if Zeq_bool i0 i then
(i0, v) :: a1
else
(i0, v0) :: (updateIndexedComp a1 i v)
| nil => (i, v) :: nil
end.
match a with
| (i0, v0)::a1 =>
if Zeq_bool i0 i then
(i0, v) :: a1
else
(i0, v0) :: (updateIndexedComp a1 i v)
| nil => (i, v) :: nil
end.
update the field f of record r by value v: r.f := v
Function updateSelectedComp (r: list (idnum * value)) (f : idnum) (v: value): list (idnum * value) :=
match r with
| (f1, v1) :: r1 =>
if beq_nat f1 f then
(f1,v) :: r1
else
(f1, v1) :: (updateSelectedComp r1 f v)
| nil => (f, v) :: nil
end.
Function arrayUpdate (a: value) (i: arrindex) (v: value): option value :=
match a with
| Undefined => Some (ArrayV (updateIndexedComp nil i v))
| ArrayV arrObj => Some (ArrayV (updateIndexedComp arrObj i v))
| _ => None
end.
match r with
| (f1, v1) :: r1 =>
if beq_nat f1 f then
(f1,v) :: r1
else
(f1, v1) :: (updateSelectedComp r1 f v)
| nil => (f, v) :: nil
end.
Function arrayUpdate (a: value) (i: arrindex) (v: value): option value :=
match a with
| Undefined => Some (ArrayV (updateIndexedComp nil i v))
| ArrayV arrObj => Some (ArrayV (updateIndexedComp arrObj i v))
| _ => None
end.
update the field f of record r by value v: r.f := v
Function recordUpdate (r: value) (f : idnum) (v: value): option value :=
match r with
| Undefined => Some (RecordV (updateSelectedComp nil f v))
| RecordV recObj => Some (RecordV (updateSelectedComp recObj f v))
| _ => None
end.
match r with
| Undefined => Some (RecordV (updateSelectedComp nil f v))
| RecordV recObj => Some (RecordV (updateSelectedComp recObj f v))
| _ => None
end.
update name with new value in the state and return newly updated state
Inductive storeUpdate: symTab -> state -> name -> value -> Ret state -> Prop :=
| SU_Identifier: forall s x v s1 st n,
updateG s x v = Some s1 ->
storeUpdate st s (Identifier n x) v (OK s1)
| SU_Indexed_Component_xRTE: forall st s x msg n e v,
evalName st s x (RTE msg) ->
storeUpdate st s (IndexedComponent n x e) v (RTE msg)
| SU_Indexed_Component_eRTE: forall st s x a e msg n v,
evalName st s x (OK (ArrayV a)) \/ evalName st s x (OK Undefined) ->
evalExp st s e (RTE msg) ->
storeUpdate st s (IndexedComponent n x e) v (RTE msg)
| SU_Indexed_Component_Range_RTE: forall st s x a e i t l u n v,
evalName st s x (OK (ArrayV a)) \/ evalName st s x (OK Undefined) ->
evalExp st s e (OK (Int i)) ->
fetch_exp_type (name_astnum x) st = Some (Array_Type t) ->
extract_array_index_range st t (Range l u) ->
rangeCheck i l u (RTE RangeError) ->
storeUpdate st s (IndexedComponent n x e) v (RTE RangeError)
| SU_Indexed_Component: forall st s x arrObj a e i t l u v a1 s1 n,
evalName st s x (OK arrObj) ->
arrObj = (ArrayV a) \/ arrObj = Undefined ->
evalExp st s e (OK (Int i)) ->
fetch_exp_type (name_astnum x) st = Some (Array_Type t) ->
extract_array_index_range st t (Range l u) ->
rangeCheck i l u (OK (Int i)) ->
arrayUpdate arrObj i v = (Some (ArrayV a1)) ->
storeUpdate st s x (ArrayV a1) s1 ->
storeUpdate st s (IndexedComponent n x e) v s1
| SU_Selected_Component_xRTE: forall st s x msg n f v,
evalName st s x (RTE msg) ->
storeUpdate st s (SelectedComponent n x f) v (RTE msg)
| SU_Selected_Component: forall st s x recObj r f v r1 s1 n,
evalName st s x (OK recObj) ->
recObj = (RecordV r) \/ recObj = Undefined ->
recordUpdate recObj f v = Some (RecordV r1) ->
storeUpdate st s x (RecordV r1) s1 ->
storeUpdate st s (SelectedComponent n x f) v s1.
| SU_Identifier: forall s x v s1 st n,
updateG s x v = Some s1 ->
storeUpdate st s (Identifier n x) v (OK s1)
| SU_Indexed_Component_xRTE: forall st s x msg n e v,
evalName st s x (RTE msg) ->
storeUpdate st s (IndexedComponent n x e) v (RTE msg)
| SU_Indexed_Component_eRTE: forall st s x a e msg n v,
evalName st s x (OK (ArrayV a)) \/ evalName st s x (OK Undefined) ->
evalExp st s e (RTE msg) ->
storeUpdate st s (IndexedComponent n x e) v (RTE msg)
| SU_Indexed_Component_Range_RTE: forall st s x a e i t l u n v,
evalName st s x (OK (ArrayV a)) \/ evalName st s x (OK Undefined) ->
evalExp st s e (OK (Int i)) ->
fetch_exp_type (name_astnum x) st = Some (Array_Type t) ->
extract_array_index_range st t (Range l u) ->
rangeCheck i l u (RTE RangeError) ->
storeUpdate st s (IndexedComponent n x e) v (RTE RangeError)
| SU_Indexed_Component: forall st s x arrObj a e i t l u v a1 s1 n,
evalName st s x (OK arrObj) ->
arrObj = (ArrayV a) \/ arrObj = Undefined ->
evalExp st s e (OK (Int i)) ->
fetch_exp_type (name_astnum x) st = Some (Array_Type t) ->
extract_array_index_range st t (Range l u) ->
rangeCheck i l u (OK (Int i)) ->
arrayUpdate arrObj i v = (Some (ArrayV a1)) ->
storeUpdate st s x (ArrayV a1) s1 ->
storeUpdate st s (IndexedComponent n x e) v s1
| SU_Selected_Component_xRTE: forall st s x msg n f v,
evalName st s x (RTE msg) ->
storeUpdate st s (SelectedComponent n x f) v (RTE msg)
| SU_Selected_Component: forall st s x recObj r f v r1 s1 n,
evalName st s x (OK recObj) ->
recObj = (RecordV r) \/ recObj = Undefined ->
recordUpdate recObj f v = Some (RecordV r1) ->
storeUpdate st s x (RecordV r1) s1 ->
storeUpdate st s (SelectedComponent n x f) v s1.
Statement Evaluation
Copy In
Inductive copyIn: symTab -> state -> frame -> list paramSpec -> list exp -> Ret frame -> Prop :=
| CopyIn_Nil : forall st s f,
copyIn st s f nil nil (OK f)
| CopyIn_Mode_In_eRTE: forall param st s e msg f lparam le,
param.(parameter_mode) = In ->
evalExp st s e (RTE msg) ->
copyIn st s f (param :: lparam) (e :: le) (RTE msg)
| CopyIn_Mode_In_NoRange: forall param st s e v f f' lparam le f'',
param.(parameter_mode) = In ->
evalExp st s e (OK v) ->
v <> Undefined ->
is_range_constrainted_type (param.(parameter_subtype_mark)) = false ->
push f param.(parameter_name) v = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) (e :: le) f''
| CopyIn_Mode_In_Range_RTE: forall param st s e v l u f lparam le,
param.(parameter_mode) = In ->
evalExp st s e (OK (Int v)) ->
extract_subtype_range st (param.(parameter_subtype_mark)) (Range l u) ->
rangeCheck v l u (RTE RangeError) ->
copyIn st s f (param :: lparam) (e :: le) (RTE RangeError)
| CopyIn_Mode_In_Range: forall param st s e v l u f f' lparam le f'',
param.(parameter_mode) = In ->
evalExp st s e (OK (Int v)) ->
extract_subtype_range st (param.(parameter_subtype_mark)) (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
push f param.(parameter_name) (Int v) = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) (e :: le) f''
| CopyIn_Mode_InOut_eRTE: forall param st s nm msg f lparam n le,
param.(parameter_mode) = In_Out ->
evalName st s nm (RTE msg) ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) (RTE msg)
| CopyIn_Mode_InOut_NoRange: forall param st s nm v f f' lparam le f'' n,
param.(parameter_mode) = In_Out ->
evalName st s nm (OK v) ->
v <> Undefined ->
is_range_constrainted_type (param.(parameter_subtype_mark)) = false ->
push f param.(parameter_name) v = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) f''
| CopyIn_Mode_InOut_Range_RTE: forall param st s nm v l u f lparam le n,
param.(parameter_mode) = In_Out ->
evalName st s nm (OK (Int v)) ->
extract_subtype_range st (param.(parameter_subtype_mark)) (Range l u) ->
rangeCheck v l u (RTE RangeError) ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) (RTE RangeError)
| CopyIn_Mode_InOut_Range: forall param st s nm v l u f f' lparam le f'' n,
param.(parameter_mode) = In_Out ->
evalName st s nm (OK (Int v)) ->
extract_subtype_range st (param.(parameter_subtype_mark)) (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
push f param.(parameter_name) (Int v) = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) f''
| CopyIn_Mode_Out: forall param f f' st s lparam le f'' n nm,
param.(parameter_mode) = Out ->
push f param.(parameter_name) Undefined = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) f''.
| CopyIn_Nil : forall st s f,
copyIn st s f nil nil (OK f)
| CopyIn_Mode_In_eRTE: forall param st s e msg f lparam le,
param.(parameter_mode) = In ->
evalExp st s e (RTE msg) ->
copyIn st s f (param :: lparam) (e :: le) (RTE msg)
| CopyIn_Mode_In_NoRange: forall param st s e v f f' lparam le f'',
param.(parameter_mode) = In ->
evalExp st s e (OK v) ->
v <> Undefined ->
is_range_constrainted_type (param.(parameter_subtype_mark)) = false ->
push f param.(parameter_name) v = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) (e :: le) f''
| CopyIn_Mode_In_Range_RTE: forall param st s e v l u f lparam le,
param.(parameter_mode) = In ->
evalExp st s e (OK (Int v)) ->
extract_subtype_range st (param.(parameter_subtype_mark)) (Range l u) ->
rangeCheck v l u (RTE RangeError) ->
copyIn st s f (param :: lparam) (e :: le) (RTE RangeError)
| CopyIn_Mode_In_Range: forall param st s e v l u f f' lparam le f'',
param.(parameter_mode) = In ->
evalExp st s e (OK (Int v)) ->
extract_subtype_range st (param.(parameter_subtype_mark)) (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
push f param.(parameter_name) (Int v) = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) (e :: le) f''
| CopyIn_Mode_InOut_eRTE: forall param st s nm msg f lparam n le,
param.(parameter_mode) = In_Out ->
evalName st s nm (RTE msg) ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) (RTE msg)
| CopyIn_Mode_InOut_NoRange: forall param st s nm v f f' lparam le f'' n,
param.(parameter_mode) = In_Out ->
evalName st s nm (OK v) ->
v <> Undefined ->
is_range_constrainted_type (param.(parameter_subtype_mark)) = false ->
push f param.(parameter_name) v = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) f''
| CopyIn_Mode_InOut_Range_RTE: forall param st s nm v l u f lparam le n,
param.(parameter_mode) = In_Out ->
evalName st s nm (OK (Int v)) ->
extract_subtype_range st (param.(parameter_subtype_mark)) (Range l u) ->
rangeCheck v l u (RTE RangeError) ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) (RTE RangeError)
| CopyIn_Mode_InOut_Range: forall param st s nm v l u f f' lparam le f'' n,
param.(parameter_mode) = In_Out ->
evalName st s nm (OK (Int v)) ->
extract_subtype_range st (param.(parameter_subtype_mark)) (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
push f param.(parameter_name) (Int v) = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) f''
| CopyIn_Mode_Out: forall param f f' st s lparam le f'' n nm,
param.(parameter_mode) = Out ->
push f param.(parameter_name) Undefined = f' ->
copyIn st s f' lparam le f'' ->
copyIn st s f (param :: lparam) ((Name n nm) :: le) f''.
Copy_out st s prefix lparams lexp s' means that s' is the result of
copying Out params of the currently finished procedure of prefix
into there output variables. More precisely:
- prefix is a portion of stack where only the parameters of the procedure are stored;
- lparams is the static specification of the parameters of the procedure;
- lexp is the list of original expressions given as parameter of the procedure (this is where one can find in which variables "out" parameters must be copied);
- s is the portion of the stack which needs to be updated and returned by the procedure, more precisely: it contains the global parameters + the local environment of the colling procedure;
- s' is the resulting state.
Copy Out
Inductive copyOut: symTab -> state -> frame -> list paramSpec -> list exp -> Ret state -> Prop :=
| CopyOut_Nil : forall st s f,
copyOut st s f nil nil (OK s)
| CopyOut_Mode_Out_nRTE: forall param f v n st t s nm msg lparam lexp,
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some v ->
v <> Undefined ->
fetch_exp_type n st = Some t ->
is_range_constrainted_type t = false ->
storeUpdate st s nm v (RTE msg) ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) (RTE msg)
| CopyOut_Mode_Out_NoRange: forall param f v n st t s nm s' lparam lexp s'',
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some v ->
v <> Undefined ->
fetch_exp_type n st = Some t ->
is_range_constrainted_type t = false ->
storeUpdate st s nm v (OK s') ->
copyOut st s' f lparam lexp s'' ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) s''
| CopyOut_Mode_Out_Range_RTE: forall param f v n st t l u s lparam nm lexp,
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some (Int v) ->
fetch_exp_type n st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (RTE RangeError) ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) (RTE RangeError)
| CopyOut_Mode_Out_Range_nRTE: forall param f v n st t l u s nm msg lparam lexp,
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some (Int v) ->
fetch_exp_type n st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
storeUpdate st s nm (Int v) (RTE msg) ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) (RTE msg)
| CopyOut_Mode_Out_Range: forall param f v n st t l u s nm s' lparam lexp s'',
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some (Int v) ->
fetch_exp_type n st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
storeUpdate st s nm (Int v) (OK s') ->
copyOut st s' f lparam lexp s'' ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) s''
| CopyOut_Mode_In: forall param st s f lparam lexp s' e,
param.(parameter_mode) = In ->
copyOut st s f lparam lexp s' ->
copyOut st s f (param :: lparam) (e :: lexp) s'.
| CopyOut_Nil : forall st s f,
copyOut st s f nil nil (OK s)
| CopyOut_Mode_Out_nRTE: forall param f v n st t s nm msg lparam lexp,
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some v ->
v <> Undefined ->
fetch_exp_type n st = Some t ->
is_range_constrainted_type t = false ->
storeUpdate st s nm v (RTE msg) ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) (RTE msg)
| CopyOut_Mode_Out_NoRange: forall param f v n st t s nm s' lparam lexp s'',
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some v ->
v <> Undefined ->
fetch_exp_type n st = Some t ->
is_range_constrainted_type t = false ->
storeUpdate st s nm v (OK s') ->
copyOut st s' f lparam lexp s'' ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) s''
| CopyOut_Mode_Out_Range_RTE: forall param f v n st t l u s lparam nm lexp,
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some (Int v) ->
fetch_exp_type n st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (RTE RangeError) ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) (RTE RangeError)
| CopyOut_Mode_Out_Range_nRTE: forall param f v n st t l u s nm msg lparam lexp,
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some (Int v) ->
fetch_exp_type n st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
storeUpdate st s nm (Int v) (RTE msg) ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) (RTE msg)
| CopyOut_Mode_Out_Range: forall param f v n st t l u s nm s' lparam lexp s'',
param.(parameter_mode) = Out \/ param.(parameter_mode) = In_Out ->
fetch param.(parameter_name) f = Some (Int v) ->
fetch_exp_type n st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
storeUpdate st s nm (Int v) (OK s') ->
copyOut st s' f lparam lexp s'' ->
copyOut st s f (param :: lparam) ((Name n nm) :: lexp) s''
| CopyOut_Mode_In: forall param st s f lparam lexp s' e,
param.(parameter_mode) = In ->
copyOut st s f lparam lexp s' ->
copyOut st s f (param :: lparam) (e :: lexp) s'.
cut_until s n s' s'' means cutting the stack s until to a frame
whose corresponding procedure's nested declaration level is less
than n, and s' is a stack with all its frame's corresponding procedure's
nested declaration level greater or equal n, and s'' is a stack holds
frames whose procedure's nested declaration levels are less than n,
and s = s' ++ s'';
Inductive cutUntil: state -> scope_level -> state -> state -> Prop :=
| CutUntil_Nil: forall n,
cutUntil nil n nil nil
| CutUntil_Head: forall f n s,
(level_of f) < n ->
cutUntil (f :: s) n nil (f :: s)
| CutUntil_Tail: forall f n s s' s'',
~ (level_of f < n) ->
cutUntil s n s' s'' ->
cutUntil (f :: s) n (f :: s') s''.
Lemma cut_until_uniqueness: forall s n intact_s' s' intact_s'' s'',
cutUntil s n intact_s' s' ->
cutUntil s n intact_s'' s'' ->
intact_s' = intact_s'' /\ s' = s''.
Proof.
intros s n intact_s' s' intact_s'' s'' H; revert intact_s'' s''.
induction H; intros;
match goal with
| [H: cutUntil nil _ _ _ |- _] => inversion H
| [H: cutUntil (?f :: ?s) _ _ _ |- _] => inversion H
end; smack;
specialize (IHcutUntil _ _ H8); smack.
Qed.
| CutUntil_Nil: forall n,
cutUntil nil n nil nil
| CutUntil_Head: forall f n s,
(level_of f) < n ->
cutUntil (f :: s) n nil (f :: s)
| CutUntil_Tail: forall f n s s' s'',
~ (level_of f < n) ->
cutUntil s n s' s'' ->
cutUntil (f :: s) n (f :: s') s''.
Lemma cut_until_uniqueness: forall s n intact_s' s' intact_s'' s'',
cutUntil s n intact_s' s' ->
cutUntil s n intact_s'' s'' ->
intact_s' = intact_s'' /\ s' = s''.
Proof.
intros s n intact_s' s' intact_s'' s'' H; revert intact_s'' s''.
induction H; intros;
match goal with
| [H: cutUntil nil _ _ _ |- _] => inversion H
| [H: cutUntil (?f :: ?s) _ _ _ |- _] => inversion H
end; smack;
specialize (IHcutUntil _ _ H8); smack.
Qed.
in a statement evaluation, whenever a run time error is detected in
the evaluation of its sub-statements or sub-component, the
evaluation is terminated and return a run-time error; otherwise,
evaluate the statement into a normal state.
- in the evaluation for assignment statement (Assign n x e),
first, check if it's needed to do range check on the right side (e) of the assignment, case 1: (is_range_constrainted_type t = false) means no range check needed for the value of expression e as the type of the left side of the assignment is not a range constrainted type, case 2: (extract_subtype_range st t (Range l u)) means left side of the assignment is a name expression of range constrainted type whose range is between l and u, so a range check is required on the value of expression e;second, if there is no range check required for e, then do expression evaluation directly on e and update the value of x if there is no run-time errors during their evaluation; if there is a range check required for e, then a range check should be performed on the evaluation value of e before it's assigned to the left side (x) of the assignment;please note that the range check for the value of expression e is verified against the target type taken from the left side (x) of the assignment, that's why the range check for expression e is enforced at the level of assignment statement even though the RangeCheck flag is set on the expression e;
- in the store update storeUpdate_rt for indexed component (e.g. a(i):=v) or selected
component (e.g. r.f := v),
if the value of array a (or value of record r) is Undefined, then create a new aggregate array value with its ith element having value v (or create a new record value with its field f having value v), and assign this new aggregate value to array variable a (or record variable r);if the value of array a (or value of record r) is already defined, then update the ith element of its array value (or update the filed f of its record value), and assign the updated aggregate value to array variable a (or record variable r);
- in the store update storeUpdate_rt for indexed component (e.g. a(i):=v), a range check is required to be performed on the value of index expression i before it's used to update the array value;
evalStmt
Inductive evalStmt: symTab -> state -> stmt -> Ret state -> Prop :=
| EvalNull: forall st s,
evalStmt st s Null (OK s)
| EvalAssign_RTE: forall st s e msg n x,
evalExp st s e (RTE msg) ->
evalStmt st s (Assign n x e) (RTE msg)
| EvalAssign: forall st s e v x t s1 n,
evalExp st s e (OK v) ->
v <> Undefined ->
fetch_exp_type (name_astnum x) st = Some t ->
is_range_constrainted_type t = false ->
storeUpdate st s x v s1 ->
evalStmt st s (Assign n x e) s1
| EvalAssign_Range_RTE: forall st s e v x t l u n,
evalExp st s e (OK (Int v)) ->
fetch_exp_type (name_astnum x) st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (RTE RangeError) ->
evalStmt st s (Assign n x e) (RTE RangeError)
| EvalAssign_Range: forall st s e v x t l u s1 n,
evalExp st s e (OK (Int v)) ->
fetch_exp_type (name_astnum x) st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
storeUpdate st s x (Int v) s1 ->
evalStmt st s (Assign n x e) s1
| EvalIf_RTE: forall st s b msg n c1 c2,
evalExp st s b (RTE msg) ->
evalStmt st s (If n b c1 c2) (RTE msg)
| EvalIf_True: forall st s b c1 s1 n c2,
evalExp st s b (OK (Bool true)) ->
evalStmt st s c1 s1 ->
evalStmt st s (If n b c1 c2) s1
| EvalIf_False: forall st s b c2 s1 n c1,
evalExp st s b (OK (Bool false)) ->
evalStmt st s c2 s1 ->
evalStmt st s (If n b c1 c2) s1
| EvalWhile_RTE: forall st s b msg n c,
evalExp st s b (RTE msg) ->
evalStmt st s (While n b c) (RTE msg)
| EvalWhile_True_RTE: forall st s b c msg n,
evalExp st s b (OK (Bool true)) ->
evalStmt st s c (RTE msg) ->
evalStmt st s (While n b c) (RTE msg)
| EvalWhile_True: forall st s b c s1 n s2,
evalExp st s b (OK (Bool true)) ->
evalStmt st s c (OK s1) ->
evalStmt st s1 (While n b c) s2 ->
evalStmt st s (While n b c) s2
| EvalWhile_False: forall st s b n c,
evalExp st s b (OK (Bool false)) ->
evalStmt st s (While n b c) (OK s)
| EvalCall_Args_RTE: forall p st n0 pb s args msg n pn,
fetch_proc p st = Some (n0, pb) ->
copyIn st s (newFrame n) (procedure_parameter_profile pb) args (RTE msg) ->
evalStmt st s (Call n pn p args) (RTE msg)
| EvalCall_Decl_RTE: forall p st n0 pb s args f intact_s s1 msg n pn,
fetch_proc p st = Some (n0, pb) ->
copyIn st s (newFrame n) (procedure_parameter_profile pb) args (OK f) ->
cutUntil s n intact_s s1 ->
evalDecl st s1 f (procedure_declarative_part pb) (RTE msg) ->
evalStmt st s (Call n pn p args) (RTE msg)
| EvalCall_Body_RTE: forall p st n0 pb s args f intact_s s1 f1 msg n pn,
fetch_proc p st = Some (n0, pb) ->
copyIn st s (newFrame n) (procedure_parameter_profile pb) args (OK f) ->
cutUntil s n intact_s s1 ->
evalDecl st s1 f (procedure_declarative_part pb) (OK f1) ->
evalStmt st (f1 :: s1) (procedure_statements pb) (RTE msg) ->
evalStmt st s (Call n pn p args) (RTE msg)
| EvalCall: forall p st n0 pb s args f intact_s s1 f1 s2 locals_section params_section s3 s4 n pn,
fetch_proc p st = Some (n0, pb) ->
copyIn st s (newFrame n) (procedure_parameter_profile pb) args (OK f) ->
cutUntil s n intact_s s1 ->
evalDecl st s1 f (procedure_declarative_part pb) (OK f1) ->
evalStmt st (f1 :: s1) (procedure_statements pb) (OK s2) ->
s2 = (n, locals_section ++ params_section) :: s3 ->
List.length (store_of f) = List.length params_section ->
copyOut st (intact_s ++ s3) (n, params_section) (procedure_parameter_profile pb) args s4 ->
evalStmt st s (Call n pn p args) s4
| EvalSeq_RTE: forall st s c1 msg n c2,
evalStmt st s c1 (RTE msg) ->
evalStmt st s (Seq n c1 c2) (RTE msg)
| EvalSeq: forall st s c1 s1 c2 s2 n,
evalStmt st s c1 (OK s1) ->
evalStmt st s1 c2 s2 ->
evalStmt st s (Seq n c1 c2) s2.
| EvalNull: forall st s,
evalStmt st s Null (OK s)
| EvalAssign_RTE: forall st s e msg n x,
evalExp st s e (RTE msg) ->
evalStmt st s (Assign n x e) (RTE msg)
| EvalAssign: forall st s e v x t s1 n,
evalExp st s e (OK v) ->
v <> Undefined ->
fetch_exp_type (name_astnum x) st = Some t ->
is_range_constrainted_type t = false ->
storeUpdate st s x v s1 ->
evalStmt st s (Assign n x e) s1
| EvalAssign_Range_RTE: forall st s e v x t l u n,
evalExp st s e (OK (Int v)) ->
fetch_exp_type (name_astnum x) st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (RTE RangeError) ->
evalStmt st s (Assign n x e) (RTE RangeError)
| EvalAssign_Range: forall st s e v x t l u s1 n,
evalExp st s e (OK (Int v)) ->
fetch_exp_type (name_astnum x) st = Some t ->
extract_subtype_range st t (Range l u) ->
rangeCheck v l u (OK (Int v)) ->
storeUpdate st s x (Int v) s1 ->
evalStmt st s (Assign n x e) s1
| EvalIf_RTE: forall st s b msg n c1 c2,
evalExp st s b (RTE msg) ->
evalStmt st s (If n b c1 c2) (RTE msg)
| EvalIf_True: forall st s b c1 s1 n c2,
evalExp st s b (OK (Bool true)) ->
evalStmt st s c1 s1 ->
evalStmt st s (If n b c1 c2) s1
| EvalIf_False: forall st s b c2 s1 n c1,
evalExp st s b (OK (Bool false)) ->
evalStmt st s c2 s1 ->
evalStmt st s (If n b c1 c2) s1
| EvalWhile_RTE: forall st s b msg n c,
evalExp st s b (RTE msg) ->
evalStmt st s (While n b c) (RTE msg)
| EvalWhile_True_RTE: forall st s b c msg n,
evalExp st s b (OK (Bool true)) ->
evalStmt st s c (RTE msg) ->
evalStmt st s (While n b c) (RTE msg)
| EvalWhile_True: forall st s b c s1 n s2,
evalExp st s b (OK (Bool true)) ->
evalStmt st s c (OK s1) ->
evalStmt st s1 (While n b c) s2 ->
evalStmt st s (While n b c) s2
| EvalWhile_False: forall st s b n c,
evalExp st s b (OK (Bool false)) ->
evalStmt st s (While n b c) (OK s)
| EvalCall_Args_RTE: forall p st n0 pb s args msg n pn,
fetch_proc p st = Some (n0, pb) ->
copyIn st s (newFrame n) (procedure_parameter_profile pb) args (RTE msg) ->
evalStmt st s (Call n pn p args) (RTE msg)
| EvalCall_Decl_RTE: forall p st n0 pb s args f intact_s s1 msg n pn,
fetch_proc p st = Some (n0, pb) ->
copyIn st s (newFrame n) (procedure_parameter_profile pb) args (OK f) ->
cutUntil s n intact_s s1 ->
evalDecl st s1 f (procedure_declarative_part pb) (RTE msg) ->
evalStmt st s (Call n pn p args) (RTE msg)
| EvalCall_Body_RTE: forall p st n0 pb s args f intact_s s1 f1 msg n pn,
fetch_proc p st = Some (n0, pb) ->
copyIn st s (newFrame n) (procedure_parameter_profile pb) args (OK f) ->
cutUntil s n intact_s s1 ->
evalDecl st s1 f (procedure_declarative_part pb) (OK f1) ->
evalStmt st (f1 :: s1) (procedure_statements pb) (RTE msg) ->
evalStmt st s (Call n pn p args) (RTE msg)
| EvalCall: forall p st n0 pb s args f intact_s s1 f1 s2 locals_section params_section s3 s4 n pn,
fetch_proc p st = Some (n0, pb) ->
copyIn st s (newFrame n) (procedure_parameter_profile pb) args (OK f) ->
cutUntil s n intact_s s1 ->
evalDecl st s1 f (procedure_declarative_part pb) (OK f1) ->
evalStmt st (f1 :: s1) (procedure_statements pb) (OK s2) ->
s2 = (n, locals_section ++ params_section) :: s3 ->
List.length (store_of f) = List.length params_section ->
copyOut st (intact_s ++ s3) (n, params_section) (procedure_parameter_profile pb) args s4 ->
evalStmt st s (Call n pn p args) s4
| EvalSeq_RTE: forall st s c1 msg n c2,
evalStmt st s c1 (RTE msg) ->
evalStmt st s (Seq n c1 c2) (RTE msg)
| EvalSeq: forall st s c1 s1 c2 s2 n,
evalStmt st s c1 (OK s1) ->
evalStmt st s1 c2 s2 ->
evalStmt st s (Seq n c1 c2) s2.