Changeset 1535 for src/RTLabs
- Timestamp:
- Nov 23, 2011, 12:07:01 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/semantics.ma
r1369 r1535 18 18 ; locals : register_env val 19 19 ; next : label 20 ; next_ok: present ?? (f_graph func) next 20 21 ; sp : block 21 22 ; retdst : option register 22 23 }. 23 24 24 definition adv : label → frame→ frame ≝25 λl,f . mk_frame (func f) (locals f) l(sp f) (retdst f).25 definition adv : ∀l:label. ∀f:frame. present ?? (f_graph (func f)) l → frame ≝ 26 λl,f,p. mk_frame (func f) (locals f) l p (sp f) (retdst f). 26 27 27 28 inductive state : Type[0] ≝ … … 48 49 λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ]. 49 50 50 definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.51 definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m. 51 52 52 53 definition init_locals : list (register × typ) → register_env val ≝ … … 90 91 match st with 91 92 [ State f fs m ⇒ 92 ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (f_graph (func f)) (next f));93 match s with94 [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉95 | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉96 | St_const r cst l ⇒ 93 let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in 94 match s return λs. labels_present ? s → ? with 95 [ St_skip l ⇒ λH. ret ? 〈E0, build_state f fs m l ?〉 96 | St_cost cl l ⇒ λH. ret ? 〈Echarge cl, build_state f fs m l ?〉 97 | St_const r cst l ⇒ λH. 97 98 ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst); 98 99 ! locals ← reg_store r v (locals f); 99 ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉100 | St_op1 _ _ op dst src l ⇒ 100 ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 101 | St_op1 _ _ op dst src l ⇒ λH. 101 102 ! v ← reg_retrieve (locals f) src; 102 103 ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v); 103 104 ! locals ← reg_store dst v' (locals f); 104 ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉105 | St_op2 op dst src1 src2 l ⇒ 105 ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 106 | St_op2 op dst src1 src2 l ⇒ λH. 106 107 ! v1 ← reg_retrieve (locals f) src1; 107 108 ! v2 ← reg_retrieve (locals f) src2; 108 109 ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2); 109 110 ! locals ← reg_store dst v' (locals f); 110 ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉111 | St_load chunk addr dst l ⇒ 111 ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 112 | St_load chunk addr dst l ⇒ λH. 112 113 ! vaddr ← reg_retrieve (locals f) addr; 113 114 ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr); 114 115 ! locals ← reg_store dst v (locals f); 115 ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉116 | St_store chunk addr src l ⇒ 116 ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 117 | St_store chunk addr src l ⇒ λH. 117 118 ! vaddr ← reg_retrieve (locals f) addr; 118 119 ! v ← reg_retrieve (locals f) src; 119 120 ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v); 120 ret ? 〈E0, build_state f fs m' l 〉121 | St_call_id id args dst l ⇒ 121 ret ? 〈E0, build_state f fs m' l ?〉 122 | St_call_id id args dst l ⇒ λH. 122 123 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); 123 124 ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); 124 125 ! vs ← mmap ?? (reg_retrieve (locals f)) args; 125 ret ? 〈E0, Callstate fd vs dst (adv l f ::fs) m〉126 | St_call_ptr frs args dst l ⇒ 126 ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉 127 | St_call_ptr frs args dst l ⇒ λH. 127 128 ! fv ← reg_retrieve (locals f) frs; 128 129 ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv); 129 130 ! vs ← mmap ?? (reg_retrieve (locals f)) args; 130 ret ? 〈E0, Callstate fd vs dst (adv l f ::fs) m〉131 | St_tailcall_id id args ⇒ 131 ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉 132 | St_tailcall_id id args ⇒ λH. 132 133 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); 133 134 ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); 134 135 ! vs ← mmap ?? (reg_retrieve (locals f)) args; 135 136 ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉 136 | St_tailcall_ptr frs args ⇒ 137 | St_tailcall_ptr frs args ⇒ λH. 137 138 ! fv ← reg_retrieve (locals f) frs; 138 139 ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv); … … 140 141 ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉 141 142 142 | St_cond src ltrue lfalse ⇒ 143 | St_cond src ltrue lfalse ⇒ λH. 143 144 ! v ← reg_retrieve (locals f) src; 144 145 ! b ← eval_bool_of_val v; 145 ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse) 〉146 147 | St_jumptable r ls ⇒ 146 ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉 147 148 | St_jumptable r ls ⇒ λH. 148 149 ! v ← reg_retrieve (locals f) r; 149 150 match v with 150 151 [ Vint _ i ⇒ 151 ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls); 152 ret ? 〈E0, build_state f fs m l〉 152 match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with 153 [ None ⇒ λ_. Wrong ??? (msg BadJumpTable) 154 | Some l ⇒ λE. ret ? 〈E0, build_state f fs m l ?〉 155 ] (refl ??) 153 156 | _ ⇒ Wrong ??? (msg BadJumpValue) 154 157 ] 155 158 156 | St_return ⇒ 159 | St_return ⇒ λH. 157 160 ! v ← match f_result (func f) with 158 161 [ None ⇒ ret ? (None ?) … … 163 166 ]; 164 167 ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉 165 ] 168 ] (f_closed (func f) (next f) s ?) 166 169 | Callstate fd params dst fs m ⇒ 167 170 match fd with … … 171 174 here *) 172 175 let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in 173 ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉176 ret ? 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉 174 177 | External fn ⇒ 175 178 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)); … … 186 189 | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch) 187 190 | Some v' ⇒ reg_store d v' (locals f) ] ]; 188 ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉191 ret ? 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉 189 192 ] 190 ]. 193 ]. try @(next_ok f) try @lookup_lookup_present try @H 194 [ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ] 195 | whd in H; @(All_nth … H ? E) 196 | cases (f_entry fn) // 197 ] qed. 191 198 192 199 definition is_final : state → option int ≝
Note: See TracChangeset
for help on using the changeset viewer.