Changeset 755 for Deliverables/D3.3
 Timestamp:
 Apr 15, 2011, 4:26:23 PM (10 years ago)
 Location:
 Deliverables/D3.3
 Files:

 4 added
 1 edited
 3 copied
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/Cminorexperiment/semantics.ma
r754 r755 11 11 definition genv ≝ (genv_t Genv) (fundef internal_function). 12 12 13 inductive cont : Type[0] ≝14  Kstop : cont 15  Kseq : stmt → cont → cont16  Kblock : cont → cont17  Kcall : option ident → internal_function → block (* sp *) → env → cont → cont.13 inductive cont : nat → Type[0] ≝ 14  Kstop : cont O 15  Kseq : ∀n. stmt n → cont n → cont n 16  Kblock : ∀n. cont n → cont (S n) 17  Kcall : option ident → internal_function → block (* sp *) → env → ∀n. cont n → cont O. 18 18 19 19 inductive state : Type[0] ≝ 20 20  State: 21 21 ∀ f: internal_function. 22 ∀ s: stmt. 22 ∀ n: nat. 23 ∀ s: stmt n. 23 24 ∀ en: env. 24 25 ∀ m: mem. 25 26 ∀ sp: block. 26 ∀ k: cont .27 ∀ k: cont n. 27 28 state 28 29  Callstate: … … 30 31 ∀ args: list val. 31 32 ∀ m: mem. 32 ∀ k: cont .33 ∀ k: cont O. 33 34 state 34 35  Returnstate: 35 36 ∀ v: option val. 36 37 ∀ m: mem. 37 ∀ k: cont .38 ∀ k: cont O. 38 39 state. 39 40 40 41 definition mem_of_state : state → mem ≝ 41 42 λst. match st with 42 [ State _ _ _ m _ _ ⇒ m43 [ State _ _ _ _ m _ _ ⇒ m 43 44  Callstate _ _ m _ ⇒ m 44 45  Returnstate _ m _ ⇒ m … … 76 77 ]. 77 78 78 let rec k_exit (n:nat) (k:cont) on k : res cont ≝ 79 match k with 80 [ Kstop ⇒ Error ? 81  Kseq _ k' ⇒ k_exit n k' 82  Kblock k' ⇒ match n with [ O ⇒ OK ? k'  S m ⇒ k_exit m k' ] 83  Kcall _ _ _ _ _ ⇒ Error ? 84 ]. 79 let rec k_exit (n:nat) (m:Fin n) (k:cont n) on k : Sig nat cont ≝ 80 (match k return λx.λ_.Fin x → Sig nat cont with 81 [ Kstop ⇒ λm.? 82  Kseq n' _ k' ⇒ λm. k_exit ? m k' 83  Kblock n' k' ⇒ λm.match m return λx.λ_.match x with [ O ⇒ True  S y ⇒ (Fin y → Sig nat cont) → Sig nat cont ] with [ FO _ ⇒ λ_.dp ??? k'  FS n' m' ⇒ λr.r m' ] (λm'. k_exit ? m' k') 84  Kcall _ _ _ _ _ _ ⇒ λm.? 85 ]) m. 86 @(match m return λx.λ_.match x return λ_.Type[0] with [ O ⇒ Sig nat cont  S _ ⇒ True] with [ FO x ⇒ I  FS x y ⇒ I ]) 87 qed. 88 85 89 86 90 let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝ … … 92 96 ]. 93 97 94 let rec call_cont (k:cont) : cont ≝ 95 match k with 96 [ Kseq _ k' ⇒ call_cont k' 97  Kblock k' ⇒ call_cont k' 98  _ ⇒ k 99 ]. 100 101 let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝ 102 match s with 103 [ St_seq s1 s2 ⇒ 104 match find_label l s1 (Kseq s2 k) with 105 [ None ⇒ find_label l s2 k 98 let rec call_cont (n:nat) (k:cont n) on k : cont O ≝ 99 match k return λ_.λ_.cont O with 100 [ Kseq _ _ k' ⇒ call_cont ? k' 101  Kblock _ k' ⇒ call_cont ? k' 102  Kstop ⇒ Kstop 103  Kcall a b c d e f ⇒ Kcall a b c d e f 104 ]. 105 106 let rec find_label (l:ident) (n:nat) (s:stmt n) (k:cont n) on s : option (Sig nat (λn.stmt n × (cont n))) ≝ 107 (match s with 108 [ St_seq _ s1 s2 ⇒ λk. 109 match find_label l ? s1 (Kseq ? s2 k) with 110 [ None ⇒ find_label l ? s2 k 106 111  Some sk ⇒ Some ? sk 107 112 ] 108  St_ifthenelse _ s1 s2 ⇒109 match find_label l s1 k with110 [ None ⇒ find_label l s2 k113  St_ifthenelse _ _ s1 s2 ⇒ λk. 114 match find_label l ? s1 k with 115 [ None ⇒ find_label l ? s2 k 111 116  Some sk ⇒ Some ? sk 112 117 ] 113  St_loop s' ⇒ find_label l s' (Kseq (St_loops') k)114  St_block s' ⇒ find_label l s' (Kblockk)115  St_label l' s' ⇒118  St_loop _ s' ⇒ λk. find_label l ? s' (Kseq ? (St_loop ? s') k) 119  St_block _ s' ⇒ λk. find_label l ? s' (Kblock ? k) 120  St_label l' _ s' ⇒ λk. 116 121 match ident_eq l l' with 117 [ inl _ ⇒ Some ? 〈s',k〉118  inr _ ⇒ find_label l s' k119 ] 120  St_cost _ s' ⇒ find_label ls' k121  _ ⇒ None ?122 ] .122 [ inl _ ⇒ Some ? (dp … 〈s',k〉) 123  inr _ ⇒ find_label l ? s' k 124 ] 125  St_cost _ _ s' ⇒ λk. find_label l ? s' k 126  _ ⇒ λk. None ? 127 ]) k. 123 128 124 129 let rec bind_params (vs:list val) (ids:list ident) : res env ≝ … … 137 142 λge,st. 138 143 match st with 139 [ State f s en m sp k ⇒140 match swith141 [ St_skip ⇒144 [ State f n0 s en m sp k ⇒ 145 (match s return λx.λ_. cont x → IO io_out io_in (trace × state) with 146 [ St_skip n ⇒ λk. 142 147 match k with 143 148 [ Kstop ⇒ Wrong ??? 144  Kseq s' k' ⇒ ret ? 〈E0, State fs' en m sp k'〉145  Kblock k' ⇒ ret ? 〈E0, State f sen m sp k'〉149  Kseq n' s' k' ⇒ ret ? 〈E0, State f n' s' en m sp k'〉 150  Kblock n' k' ⇒ ret ? 〈E0, State f n' (St_skip ?) en m sp k'〉 146 151 (* cminor allows functions without an explicit return statement *) 147  Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉148 ] 149  St_assign id e ⇒152  Kcall a b c d e f ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (Kcall a b c d e f)〉 153 ] 154  St_assign id e n ⇒ λk. 150 155 ! 〈tr,v〉 ← eval_expr ge e en sp m; 151 ret ? 〈tr, State f St_skip(add ?? en id v) m sp k〉152  St_store chunk edst e ⇒156 ret ? 〈tr, State f n (St_skip ?) (add ?? en id v) m sp k〉 157  St_store chunk edst e n ⇒ λk. 153 158 ! 〈tr,vdst〉 ← eval_expr ge edst en sp m; 154 159 ! 〈tr',v〉 ← eval_expr ge e en sp m; 155 160 ! m' ← opt_to_res … (storev chunk m vdst v); 156 ret ? 〈tr ⧺ tr', State f St_skipen m' sp k〉157 158  St_call dst ef args sig ⇒(* XXX sig unused? *)161 ret ? 〈tr ⧺ tr', State f n (St_skip ?) en m' sp k〉 162 163  St_call dst ef args sig n ⇒ λk. (* XXX sig unused? *) 159 164 ! 〈tr,vf〉 ← eval_expr ge ef en sp m; 160 165 ! fd ← opt_to_res … (find_funct ?? ge vf); 161 166 ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args; 162 ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉163  St_tailcall ef args sig ⇒167 ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en n k)〉 168  St_tailcall ef args sig n ⇒ λk. 164 169 ! 〈tr,vf〉 ← eval_expr ge ef en sp m; 165 170 ! fd ← opt_to_res … (find_funct ?? ge vf); 166 171 ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args; 167 ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) k〉172 ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont ? k)〉 168 173 169  St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseqs2 k)〉170  St_ifthenelse e strue sfalse ⇒174  St_seq n s1 s2 ⇒ λk. ret ? 〈E0, State f n s1 en m sp (Kseq ? s2 k)〉 175  St_ifthenelse e n strue sfalse ⇒ λk. 171 176 ! 〈tr,v〉 ← eval_expr ge e en sp m; 172 177 ! b ← eval_bool_of_val v; 173 ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉 174  St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)〉 175  St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)〉 176  St_exit n ⇒ 177 ! k' ← k_exit n k; 178 ret ? 〈E0, State f St_skip en m sp k'〉 179  St_switch e cs default ⇒ 178 ret ? 〈tr, State f n (if b then strue else sfalse) en m sp k〉 179  St_loop n s ⇒ λk. ret ? 〈E0, State f n s en m sp (Kseq ? (St_loop ? s) k)〉 180  St_block n s ⇒ λk. ret ? 〈E0, State f ? s en m sp (Kblock ? k)〉 181  St_exit n x ⇒ λk. 182 match k_exit n x k with 183 [ dp n' k' ⇒ 184 ret ? 〈E0, State f ? (St_skip ?) en m sp k'〉 185 ] 186  St_switch e n cs default ⇒ λk. 180 187 ! 〈tr,v〉 ← eval_expr ge e en sp m; 181 188 match v with 182 189 [ Vint i ⇒ 183 ! k' ← k_exit (find_case ? i cs default) k; 184 ret ? 〈tr, State f St_skip en m sp k'〉 190 match k_exit ? (find_case ? i cs default) k with 191 [ dp n k' ⇒ 192 ret ? 〈tr, State f n (St_skip ?) en m sp k'〉 193 ] 185 194  _ ⇒ Wrong ??? 186 195 ] 187  St_return eo ⇒196  St_return eo n ⇒ λk. 188 197 match eo with 189 [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉198 [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont ? k)〉 190 199  Some e ⇒ 191 200 ! 〈tr,v〉 ← eval_expr ge e en sp m; 192 ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉 193 ] 194  St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉 195  St_goto l ⇒ 196 ! 〈s', k'〉 ← opt_to_res … (find_label l (f_body f) (call_cont k)); 197 ret ? 〈E0, State f s' en m sp k'〉 198  St_cost l s' ⇒ 199 ret ? 〈Echarge l, State f s' en m sp k〉 200 ] 201 ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont ? k)〉 202 ] 203  St_label l n s' ⇒ λk. ret ? 〈E0, State f ? s' en m sp k〉 204  St_goto l n ⇒ λk. 205 ! x ← opt_to_res … (find_label l ? (f_body f) (call_cont ? k)); 206 match x with [ dp n' x' ⇒ let 〈s', k'〉 ≝ x' in 207 ret ? 〈E0, State f ? s' en m sp k'〉 208 ] 209  St_cost l n s' ⇒ λk. 210 ret ? 〈Echarge l, State f n s' en m sp k〉 211 ]) k 201 212  Callstate fd args m k ⇒ 202 213 match fd with … … 204 215 let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in 205 216 ! en ← bind_params args (f_params f); 206 ret ? 〈E0, State f (f_body f) en m' sp k〉217 ret ? 〈E0, State f O (f_body f) en m' sp k〉 207 218  External fn ⇒ 208 219 ! evargs ← check_eventval_list args (sig_args (ef_sig fn)); … … 213 224  Returnstate res m k ⇒ 214 225 match k with 215 [ Kcall dst f sp en k' ⇒226 [ Kcall dst f sp en n k' ⇒ 216 227 ! en' ← match res with 217 228 [ None ⇒ match dst with [ None ⇒ OK ? en  Some _ ⇒ Error ? ] … … 219 230  Some id ⇒ OK ? (add ?? en id v) ] 220 231 ]; 221 ret ? 〈E0, State f St_skipen' m sp k'〉232 ret ? 〈E0, State f n (St_skip ?) en' m sp k'〉 222 233  _ ⇒ Wrong ??? 223 234 ] 
Deliverables/D3.3/Cminorexperiment/syntax.ma
r754 r755 12 12  Ecost : costlabel → expr → expr. 13 13 14 inductive stmt : Type[0] ≝ 15  St_skip : stmt 16  St_assign : ident → expr → stmt 17  St_store : memory_chunk → expr → expr → stmt 14 inductive Fin : nat → Type[0] ≝ 15  FO : ∀n. Fin (S n) 16  FS : ∀n. Fin n → Fin (S n). 17 18 inductive stmt : ∀blockdepth:nat. Type[0] ≝ 19  St_skip : ∀n. stmt n 20  St_assign : ident → expr → ∀n. stmt n 21  St_store : memory_chunk → expr → expr → ∀n. stmt n 18 22 (* ident for returned value, expression to identify fn, args, signature. *) 19  St_call : option ident → expr → list expr → signature → stmt20  St_tailcall : expr → list expr → signature → stmt21  St_seq : stmt → stmt → stmt22  St_ifthenelse : expr → stmt → stmt → stmt23  St_loop : stmt → stmt24  St_block : stmt → stmt25  St_exit : nat → stmt23  St_call : option ident → expr → list expr → signature → ∀n. stmt n 24  St_tailcall : expr → list expr → signature → ∀n. stmt n 25  St_seq : ∀n. stmt n → stmt n → stmt n 26  St_ifthenelse : expr → ∀n. stmt n → stmt n → stmt n 27  St_loop : ∀n. stmt n → stmt n 28  St_block : ∀n. stmt (S n) → stmt n 29  St_exit : ∀n. Fin n → stmt n 26 30 (* expr to switch on, table of 〈switch value, #blocks to exit〉, default *) 27  St_switch : expr → list (int × nat) → nat → stmt28  St_return : option expr → stmt29  St_label : ident → stmt → stmt30  St_goto : ident → stmt31  St_cost : costlabel → stmt → stmt.31  St_switch : expr → ∀n. list (int × (Fin n)) → Fin n → stmt n 32  St_return : option expr → ∀n. stmt n 33  St_label : ident → ∀n. stmt n → stmt n 34  St_goto : ident → ∀n. stmt n 35  St_cost : costlabel → ∀n. stmt n → stmt n. 32 36 33 37 record internal_function : Type[0] ≝ … … 37 41 ; f_ptrs : list ident 38 42 ; f_stacksize : nat 39 ; f_body : stmt 43 ; f_body : stmt O 40 44 }. 41 45 (* XXX: matita interpretations bug workaround *) 
Deliverables/D3.3/Cminorexperiment/test/search.ma
r751 r755 25 25 [id_search_tab] 26 26 0 ( 27 St_cost C_cost8 (28 St_seq (29 St_assign id_search_low (Cst (Ointconst (repr 0))) 27 St_cost C_cost8 ? ( 28 St_seq ? ( 29 St_assign id_search_low (Cst (Ointconst (repr 0))) ? 30 30 ) ( 31 St_seq (32 St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_size)) (Cst (Ointconst (repr 1)))) 31 St_seq ? ( 32 St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_size)) (Cst (Ointconst (repr 1)))) ? 33 33 ) ( 34 St_seq (35 St_seq (36 St_block (37 St_loop (38 St_seq (39 St_ifthenelse (Op1 Onotbool (Op2 (Ocmp Cge) (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low)))) (40 St_exit 034 St_seq ? ( 35 St_seq ? ( 36 St_block ? ( 37 St_loop ? ( 38 St_seq ? ( 39 St_ifthenelse (Op1 Onotbool (Op2 (Ocmp Cge) (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low)))) ? ( 40 St_exit ? (FO ?) 41 41 ) ( 42 St_skip )42 St_skip ? ) 43 43 ) ( 44 St_block (45 St_cost C_cost6 (46 St_seq (47 St_assign id_search_i (Op2 Odiv (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low))) (Cst (Ointconst (repr 2)))) 44 St_block ? ( 45 St_cost C_cost6 ? ( 46 St_seq ? ( 47 St_assign id_search_i (Op2 Odiv (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_high)) (Op1 Ocast8unsigned (Id id_search_low))) (Cst (Ointconst (repr 2)))) ? 48 48 ) ( 49 St_seq (50 St_ifthenelse (Op2 (Ocmp Ceq) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) (51 St_cost C_cost4 (52 St_return (Some ? (Id id_search_i)) 49 St_seq ? ( 50 St_ifthenelse (Op2 (Ocmp Ceq) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) ? ( 51 St_cost C_cost4 ? ( 52 St_return (Some ? (Id id_search_i)) ? 53 53 ) 54 54 ) ( 55 St_cost C_cost5 (56 St_skip )55 St_cost C_cost5 ? ( 56 St_skip ? ) 57 57 ) 58 58 ) ( 59 St_seq (60 St_ifthenelse (Op2 (Ocmp Cgt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) (61 St_cost C_cost2 (62 St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1)))) 59 St_seq ? ( 60 St_ifthenelse (Op2 (Ocmp Cgt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) ? ( 61 St_cost C_cost2 ? ( 62 St_assign id_search_high (Op2 Osub (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1)))) ? 63 63 ) 64 64 ) ( 65 St_cost C_cost3 (66 St_skip )65 St_cost C_cost3 ? ( 66 St_skip ? ) 67 67 ) 68 68 ) ( 69 St_ifthenelse (Op2 (Ocmp Clt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) (70 St_cost C_cost0 (71 St_assign id_search_low (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1)))) 69 St_ifthenelse (Op2 (Ocmp Clt) (Op1 Ocast8unsigned (Mem Mint8unsigned (Op2 Oaddp (Id id_search_tab) (Op2 Omul (Id id_search_i) (Cst (Ointconst (repr 1))))))) (Op1 Ocast8unsigned (Id id_search_to_find))) ? ( 70 St_cost C_cost0 ? ( 71 St_assign id_search_low (Op2 Oadd (Op1 Ocast8unsigned (Id id_search_i)) (Cst (Ointconst (repr 1)))) ? 72 72 ) 73 73 ) ( 74 St_cost C_cost1 (75 St_skip )74 St_cost C_cost1 ? ( 75 St_skip ? ) 76 76 ) 77 77 ) … … 84 84 ) 85 85 ) ( 86 St_cost C_cost7 (87 St_skip )86 St_cost C_cost7 ? ( 87 St_skip ? ) 88 88 ) 89 89 ) ( 90 St_return (Some ? (Op1 Onegint (Cst (Ointconst (repr 1))))) 90 St_return (Some ? (Op1 Onegint (Cst (Ointconst (repr 1))))) ? 91 91 ) 92 92 ) … … 106 106 [] 107 107 5 ( 108 St_cost C_cost9 (109 St_seq (110 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 0))) 108 St_cost C_cost9 ? ( 109 St_seq ? ( 110 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 0))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 0))) ? 111 111 ) ( 112 St_seq (113 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 1))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 18))) 112 St_seq ? ( 113 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 1))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 18))) ? 114 114 ) ( 115 St_seq (116 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 2))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 23))) 115 St_seq ? ( 116 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 2))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 23))) ? 117 117 ) ( 118 St_seq (119 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 3))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 57))) 118 St_seq ? ( 119 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 3))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 57))) ? 120 120 ) ( 121 St_seq (122 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 4))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 120))) 121 St_seq ? ( 122 St_store Mint8unsigned (Op2 Oaddp (Cst (Oaddrstack (repr 0))) (Op2 Omul (Cst (Ointconst (repr 4))) (Cst (Ointconst (repr 1))))) (Cst (Ointconst (repr 120))) ? 123 123 ) ( 124 St_seq (125 St_call (Some ? id_main_res) (Cst (Oaddrsymbol id_search (repr 0))) [Cst (Oaddrstack (repr 0)); Cst (Ointconst (repr 5)); Cst (Ointconst (repr 57))] (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint)) 124 St_seq ? ( 125 St_call (Some ? id_main_res) (Cst (Oaddrsymbol id_search (repr 0))) [Cst (Oaddrstack (repr 0)); Cst (Ointconst (repr 5)); Cst (Ointconst (repr 57))] (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint)) ? 126 126 ) ( 127 St_return (Some ? (Op1 Ocast8unsigned (Id id_main_res))) 127 St_return (Some ? (Op1 Ocast8unsigned (Id id_main_res))) ? 128 128 ) 129 129 )
Note: See TracChangeset
for help on using the changeset viewer.