Changeset 1153


Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (8 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
32 edited
6 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ASM

  • Deliverables/D3.3/id-lookup-branch/ASM/ASM.ma

    r985 r1153  
    9191   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
    9292   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
    93    | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]].
     93   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]
     94   ].
    9495
    9596
  • Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma

    r1098 r1153  
    147147definition RegisterSPL ≝ Register06.
    148148definition RegisterSPH ≝ Register07.
     149definition RegisterForbidden: list Register ≝
     150  [ RegisterSST; RegisterST0; RegisterST1;
     151    RegisterSPL; RegisterSPH ].
     152definition RegisterParams: list Register ≝
     153  [ Register30; Register31; Register32; Register33;
     154    Register34; Register35; Register36; Register37 ].
    149155definition Registers ≝
    150156  [Register00; Register01; Register02; Register03; Register04;
     
    167173  [Register20; Register21; Register22; Register23; Register24;
    168174   Register25; Register26; Register27].
    169 definition RegisterParameters ≝
    170   [Register30; Register31; Register32; Register33; Register34; Register35;
    171    Register36; Register37].
    172175
    173176definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    192195    ]
    193196qed.
    194    
    195 definition registers: list Register ≝
    196   [ Register00; Register01; Register02; Register03;
    197     Register04; Register05; Register06; Register07;
    198     RegisterA; RegisterB; RegisterDPL; RegisterDPH;
    199     Register10; Register11; Register12; Register13;
    200     Register14; Register15; Register16; Register17;
    201     Register20; Register21; Register22; Register23;
    202     Register24; Register25; Register26; Register27;
    203     Register30; Register31; Register32; Register33;
    204     Register34; Register35; Register36; Register37;
    205     RegisterSST; RegisterST0; RegisterST1;
    206     RegisterSPL; RegisterSPH ].
    207    
    208 definition forbidden_registers: list Register ≝
    209   [ RegisterSST; RegisterST0; RegisterST1;
    210     RegisterSPL; RegisterSPH ].
    211    
    212 definition parameters: list Register ≝
    213   [ Register30; Register31; Register32; Register33;
    214     Register34; Register35; Register36; Register37 ].
    215197   
    216198record RegisterMap: Type[0] ≝
     
    32423224record Eval: Type[0] ≝
    32433225{
    3244   opaccs: OpAccs → Byte → Byte → option Byte;
     3226  opaccs: OpAccs → Byte → Byte → Byte × Byte;
    32453227  op1: Op1 → Byte → Byte;
    32463228  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
    32473229}.
    32483230
    3249 axiom opaccs_implementation: OpAccs → Byte → Byte → option Byte.
     3231axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
    32503232axiom op1_implementation: Op1 → Byte → Byte.
    32513233axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
  • Deliverables/D3.3/id-lookup-branch/CHANGES

    r1065 r1153  
    7171  arbitrary decision).
    7272
     7330/08/2011:  [annotation]
     74  There is a mismatch between the capability of external functions in the
     75  OCaml and Matita code. In OCaml they can interact with the memory. In
     76  Matita (following old? CompCert) they cannot. Hence, in the semantics
     77  of intermediate languages from ERTL on, we need to recover the arguments
     78  for the function not only from the registers, but also from the stack.
  • Deliverables/D3.3/id-lookup-branch/Clight/Cexec.ma

    r1058 r1153  
    77include "Clight/TypeComparison.ma".
    88
    9 (*
    10 include "Plogic/russell_support.ma".
    11 
    12 definition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
    13   λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]].
    14 
    15 definition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (Sig A P) ≝
    16   λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a.
    17   (match a return λa'.a=a' → res (Sig A P) with
    18    [ None ⇒ λe1.?
    19    | Some b ⇒ λe1.(match b return λb'.b=b' → ? with
    20      [ Error ⇒ λ_. Error ?
    21      | OK c ⇒ λe2. OK ? (dp A P c ?)
    22      ]) (refl ? b)
    23    ]) (refl ? a).
    24 [ >e1 in p; normalize; *;
    25 | >e1 in p >e2 normalize; //
    26 ] qed.
    27 
    28 definition err_eject : ∀A.∀P: A → Prop. res (Sig A P) → res A ≝
    29   λA,P,a.match a with [ Error m ⇒ Error ? m | OK b ⇒
    30     match b with [ dp w p ⇒ OK ? w] ].
    31 
    32 definition sig_eject : ∀A.∀P: A → Prop. Sig A P → A ≝
    33   λA,P,a.match a with [ dp w p ⇒ w].
    34 
    35 coercion err_inject :
    36   ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (Sig A P) ≝ err_inject
    37   on a:option (res ?) to res (Sig ? ?).
    38 coercion err_eject : ∀A.∀P:A → Prop.∀c:res (Sig A P).res A ≝ err_eject
    39   on _c:res (Sig ? ?) to res ?.
    40 coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject
    41   on _c:Sig ? ? to ?.
    42 *)
    439definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
    4410  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
     
    181147λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
    182148
    183 (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
    184    a structurally smaller value, we break out the surrounding Expr constructor
    185    and use exec_lvalue'. *)
    186 
    187149axiom BadlyTypedTerm : String.
    188150axiom UnknownIdentifier : String.
     
    190152axiom FailedLoad : String.
    191153axiom FailedOp : String.
     154
     155(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     156   a structurally smaller value, we break out the surrounding Expr constructor
     157   and use exec_lvalue'. *)
    192158
    193159let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
     
    534500
    535501let rec make_initial_state (p:clight_program) : res (genv × state) ≝
    536   do ge ← globalenv Genv ?? p;
    537   do m0 ← init_mem Genv ?? p;
     502  do ge ← globalenv Genv ?? (fst ??) p;
     503  do m0 ← init_mem Genv ?? (fst ??) p;
    538504  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    539505  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     
    584550  | S n' ⇒
    585551      ! 〈t,s'〉 ← exec_step ge s;
    586 (*      ! 〈t,s'〉 ← match s with
    587                  [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (State f s k e (mk_mem c n p)) ]
    588                  | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Callstate fd args k (mk_mem c n p)) ]
    589                  | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ]
    590                  ] ;*)
    591       ! 〈t',s''〉 ← match s' with
    592                  [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (State f s k e (mk_mem c n p)) ]
    593                  | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Callstate fd args k (mk_mem c n p)) ]
    594                  | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ]
    595                  ] ;
    596 (*      ! 〈t',s''〉 ← exec_steps n' ge s';*)
     552      ! 〈t',s''〉 ← exec_steps n' ge s';
    597553      ret ? 〈t ⧺ t',s''〉
    598554  ]
  • Deliverables/D3.3/id-lookup-branch/Clight/CexecSound.ma

    r1058 r1153  
    533533qed.
    534534
    535 lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
     535lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? (fst ??) p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
    536536#p cases p; #fns #main #vars
    537537whd in ⊢ (???%);
  • Deliverables/D3.3/id-lookup-branch/Clight/Csem.ma

    r1058 r1153  
    11971197      step ge (State f (Scost lbl s) k e m)
    11981198           (Echarge lbl) (State f s k e m).
     1199
    11991200(*
    1200 (** * Alternate big-step semantics *)
    1201 
    1202 (** ** Big-step semantics for terminating statements and functions *)
    1203 
    1204 (** The execution of a statement produces an ``outcome'', indicating
    1205   how the execution terminated: either normally or prematurely
    1206   through the execution of a [break], [continue] or [return] statement. *)
    1207 
    1208 inductive outcome: Type[0] :=
    1209    | Out_break: outcome                 (**r terminated by [break] *)
    1210    | Out_continue: outcome              (**r terminated by [continue] *)
    1211    | Out_normal: outcome                (**r terminated normally *)
    1212    | Out_return: option val -> outcome. (**r terminated by [return] *)
    1213 
    1214 inductive out_normal_or_continue : outcome -> Prop :=
    1215   | Out_normal_or_continue_N: out_normal_or_continue Out_normal
    1216   | Out_normal_or_continue_C: out_normal_or_continue Out_continue.
    1217 
    1218 inductive out_break_or_return : outcome -> outcome -> Prop :=
    1219   | Out_break_or_return_B: out_break_or_return Out_break Out_normal
    1220   | Out_break_or_return_R: ∀ov.
    1221       out_break_or_return (Out_return ov) (Out_return ov).
    1222 
    1223 Definition outcome_switch (out: outcome) : outcome :=
    1224   match out with
    1225   | Out_break => Out_normal
    1226   | o => o
    1227   end.
    1228 
    1229 Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
    1230   match out, t with
    1231   | Out_normal, Tvoid => v = Vundef
    1232   | Out_return None, Tvoid => v = Vundef
    1233   | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v
    1234   | _, _ => False
    1235   end.
    1236 
    1237 (** [exec_stmt ge e m1 s t m2 out] describes the execution of
    1238   the statement [s].  [out] is the outcome for this execution.
    1239   [m1] is the initial memory state, [m2] the final memory state.
    1240   [t] is the trace of input/output events performed during this
    1241   evaluation. *)
    1242 
    1243 inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
    1244   | exec_Sskip:   ∀e,m.
    1245       exec_stmt e m Sskip
    1246                E0 m Out_normal
    1247   | exec_Sassign:   ∀e,m,a1,a2,loc,ofs,v2,m'.
    1248       eval_lvalue e m a1 loc ofs ->
    1249       eval_expr e m a2 v2 ->
    1250       store_value_of_type (typeof a1) m loc ofs v2 = Some m' ->
    1251       exec_stmt e m (Sassign a1 a2)
    1252                E0 m' Out_normal
    1253   | exec_Scall_none:   ∀e,m,a,al,vf,vargs,f,t,m',vres.
    1254       eval_expr e m a vf ->
    1255       eval_exprlist e m al vargs ->
    1256       Genv.find_funct ge vf = Some f ->
    1257       type_of_fundef f = typeof a ->
    1258       eval_funcall m f vargs t m' vres ->
    1259       exec_stmt e m (Scall None a al)
    1260                 t m' Out_normal
    1261   | exec_Scall_some:   ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t,m',vres,m''.
    1262       eval_lvalue e m lhs loc ofs ->
    1263       eval_expr e m a vf ->
    1264       eval_exprlist e m al vargs ->
    1265       Genv.find_funct ge vf = Some f ->
    1266       type_of_fundef f = typeof a ->
    1267       eval_funcall m f vargs t m' vres ->
    1268       store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' ->
    1269       exec_stmt e m (Scall (Some lhs) a al)
    1270                 t m'' Out_normal
    1271   | exec_Sseq_1:   ∀e,m,s1,s2,t1,m1,t2,m2,out.
    1272       exec_stmt e m s1 t1 m1 Out_normal ->
    1273       exec_stmt e m1 s2 t2 m2 out ->
    1274       exec_stmt e m (Ssequence s1 s2)
    1275                 (t1 ** t2) m2 out
    1276   | exec_Sseq_2:   ∀e,m,s1,s2,t1,m1,out.
    1277       exec_stmt e m s1 t1 m1 out ->
    1278       out <> Out_normal ->
    1279       exec_stmt e m (Ssequence s1 s2)
    1280                 t1 m1 out
    1281   | exec_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t,m',out.
    1282       eval_expr e m a v1 ->
    1283       is_true v1 (typeof a) ->
    1284       exec_stmt e m s1 t m' out ->
    1285       exec_stmt e m (Sifthenelse a s1 s2)
    1286                 t m' out
    1287   | exec_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t,m',out.
    1288       eval_expr e m a v1 ->
    1289       is_false v1 (typeof a) ->
    1290       exec_stmt e m s2 t m' out ->
    1291       exec_stmt e m (Sifthenelse a s1 s2)
    1292                 t m' out
    1293   | exec_Sreturn_none:   ∀e,m.
    1294       exec_stmt e m (Sreturn None)
    1295                E0 m (Out_return None)
    1296   | exec_Sreturn_some: ∀e,m,a,v.
    1297       eval_expr e m a v ->
    1298       exec_stmt e m (Sreturn (Some a))
    1299                E0 m (Out_return (Some v))
    1300   | exec_Sbreak:   ∀e,m.
    1301       exec_stmt e m Sbreak
    1302                E0 m Out_break
    1303   | exec_Scontinue:   ∀e,m.
    1304       exec_stmt e m Scontinue
    1305                E0 m Out_continue
    1306   | exec_Swhile_false: ∀e,m,a,s,v.
    1307       eval_expr e m a v ->
    1308       is_false v (typeof a) ->
    1309       exec_stmt e m (Swhile a s)
    1310                E0 m Out_normal
    1311   | exec_Swhile_stop: ∀e,m,a,v,s,t,m',out',out.
    1312       eval_expr e m a v ->
    1313       is_true v (typeof a) ->
    1314       exec_stmt e m s t m' out' ->
    1315       out_break_or_return out' out ->
    1316       exec_stmt e m (Swhile a s)
    1317                 t m' out
    1318   | exec_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2,m2,out.
    1319       eval_expr e m a v ->
    1320       is_true v (typeof a) ->
    1321       exec_stmt e m s t1 m1 out1 ->
    1322       out_normal_or_continue out1 ->
    1323       exec_stmt e m1 (Swhile a s) t2 m2 out ->
    1324       exec_stmt e m (Swhile a s)
    1325                 (t1 ** t2) m2 out
    1326   | exec_Sdowhile_false: ∀e,m,s,a,t,m1,out1,v.
    1327       exec_stmt e m s t m1 out1 ->
    1328       out_normal_or_continue out1 ->
    1329       eval_expr e m1 a v ->
    1330       is_false v (typeof a) ->
    1331       exec_stmt e m (Sdowhile a s)
    1332                 t m1 Out_normal
    1333   | exec_Sdowhile_stop: ∀e,m,s,a,t,m1,out1,out.
    1334       exec_stmt e m s t m1 out1 ->
    1335       out_break_or_return out1 out ->
    1336       exec_stmt e m (Sdowhile a s)
    1337                 t m1 out
    1338   | exec_Sdowhile_loop: ∀e,m,s,a,m1,m2,t1,t2,out,out1,v.
    1339       exec_stmt e m s t1 m1 out1 ->
    1340       out_normal_or_continue out1 ->
    1341       eval_expr e m1 a v ->
    1342       is_true v (typeof a) ->
    1343       exec_stmt e m1 (Sdowhile a s) t2 m2 out ->
    1344       exec_stmt e m (Sdowhile a s)
    1345                 (t1 ** t2) m2 out
    1346   | exec_Sfor_start: ∀e,m,s,a1,a2,a3,out,m1,m2,t1,t2.
    1347       a1 <> Sskip ->
    1348       exec_stmt e m a1 t1 m1 Out_normal ->
    1349       exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out ->
    1350       exec_stmt e m (Sfor a1 a2 a3 s)
    1351                 (t1 ** t2) m2 out
    1352   | exec_Sfor_false: ∀e,m,s,a2,a3,v.
    1353       eval_expr e m a2 v ->
    1354       is_false v (typeof a2) ->
    1355       exec_stmt e m (Sfor Sskip a2 a3 s)
    1356                E0 m Out_normal
    1357   | exec_Sfor_stop: ∀e,m,s,a2,a3,v,m1,t,out1,out.
    1358       eval_expr e m a2 v ->
    1359       is_true v (typeof a2) ->
    1360       exec_stmt e m s t m1 out1 ->
    1361       out_break_or_return out1 out ->
    1362       exec_stmt e m (Sfor Sskip a2 a3 s)
    1363                 t m1 out
    1364   | exec_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,m3,t1,t2,t3,out1,out.
    1365       eval_expr e m a2 v ->
    1366       is_true v (typeof a2) ->
    1367       exec_stmt e m s t1 m1 out1 ->
    1368       out_normal_or_continue out1 ->
    1369       exec_stmt e m1 a3 t2 m2 Out_normal ->
    1370       exec_stmt e m2 (Sfor Sskip a2 a3 s) t3 m3 out ->
    1371       exec_stmt e m (Sfor Sskip a2 a3 s)
    1372                 (t1 ** t2 ** t3) m3 out
    1373   | exec_Sswitch:   ∀e,m,a,t,n,sl,m1,out.
    1374       eval_expr e m a (Vint n) ->
    1375       exec_stmt e m (seq_of_labeled_statement (select_switch n sl)) t m1 out ->
    1376       exec_stmt e m (Sswitch a sl)
    1377                 t m1 (outcome_switch out)
    1378 
    1379 (** [eval_funcall m1 fd args t m2 res] describes the invocation of
    1380   function [fd] with arguments [args].  [res] is the value returned
    1381   by the call.  *)
    1382 
    1383 with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
    1384   | eval_funcall_internal: ∀m,f,vargs,t,e,m1,m2,m3,out,vres.
    1385       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
    1386       bind_parameters e m1 f.(fn_params) vargs m2 ->
    1387       exec_stmt e m2 f.(fn_body) t m3 out ->
    1388       outcome_result_value out f.(fn_return) vres ->
    1389       eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres
    1390   | eval_funcall_external: ∀m,id,targs,tres,vargs,t,vres.
    1391       event_match (external_function id targs tres) vargs t vres ->
    1392       eval_funcall m (External id targs tres) vargs t m vres.
    1393 
    1394 Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
    1395   with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
    1396 
    1397 (** ** Big-step semantics for diverging statements and functions *)
    1398 
    1399 (** Coinductive semantics for divergence.
    1400   [execinf_stmt ge e m s t] holds if the execution of statement [s]
    1401   diverges, i.e. loops infinitely.  [t] is the possibly infinite
    1402   trace of observable events performed during the execution. *)
    1403 
    1404 Coinductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop :=
    1405   | execinf_Scall_none:   ∀e,m,a,al,vf,vargs,f,t.
    1406       eval_expr e m a vf ->
    1407       eval_exprlist e m al vargs ->
    1408       Genv.find_funct ge vf = Some f ->
    1409       type_of_fundef f = typeof a ->
    1410       evalinf_funcall m f vargs t ->
    1411       execinf_stmt e m (Scall None a al) t
    1412   | execinf_Scall_some:   ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t.
    1413       eval_lvalue e m lhs loc ofs ->
    1414       eval_expr e m a vf ->
    1415       eval_exprlist e m al vargs ->
    1416       Genv.find_funct ge vf = Some f ->
    1417       type_of_fundef f = typeof a ->
    1418       evalinf_funcall m f vargs t ->
    1419       execinf_stmt e m (Scall (Some lhs) a al) t
    1420   | execinf_Sseq_1:   ∀e,m,s1,s2,t.
    1421       execinf_stmt e m s1 t ->
    1422       execinf_stmt e m (Ssequence s1 s2) t
    1423   | execinf_Sseq_2:   ∀e,m,s1,s2,t1,m1,t2.
    1424       exec_stmt e m s1 t1 m1 Out_normal ->
    1425       execinf_stmt e m1 s2 t2 ->
    1426       execinf_stmt e m (Ssequence s1 s2) (t1 *** t2)
    1427   | execinf_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t.
    1428       eval_expr e m a v1 ->
    1429       is_true v1 (typeof a) ->
    1430       execinf_stmt e m s1 t ->
    1431       execinf_stmt e m (Sifthenelse a s1 s2) t
    1432   | execinf_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t.
    1433       eval_expr e m a v1 ->
    1434       is_false v1 (typeof a) ->
    1435       execinf_stmt e m s2 t ->
    1436       execinf_stmt e m (Sifthenelse a s1 s2) t
    1437   | execinf_Swhile_body: ∀e,m,a,v,s,t.
    1438       eval_expr e m a v ->
    1439       is_true v (typeof a) ->
    1440       execinf_stmt e m s t ->
    1441       execinf_stmt e m (Swhile a s) t
    1442   | execinf_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2.
    1443       eval_expr e m a v ->
    1444       is_true v (typeof a) ->
    1445       exec_stmt e m s t1 m1 out1 ->
    1446       out_normal_or_continue out1 ->
    1447       execinf_stmt e m1 (Swhile a s) t2 ->
    1448       execinf_stmt e m (Swhile a s) (t1 *** t2)
    1449   | execinf_Sdowhile_body: ∀e,m,s,a,t.
    1450       execinf_stmt e m s t ->
    1451       execinf_stmt e m (Sdowhile a s) t
    1452   | execinf_Sdowhile_loop: ∀e,m,s,a,m1,t1,t2,out1,v.
    1453       exec_stmt e m s t1 m1 out1 ->
    1454       out_normal_or_continue out1 ->
    1455       eval_expr e m1 a v ->
    1456       is_true v (typeof a) ->
    1457       execinf_stmt e m1 (Sdowhile a s) t2 ->
    1458       execinf_stmt e m (Sdowhile a s) (t1 *** t2)
    1459   | execinf_Sfor_start_1: ∀e,m,s,a1,a2,a3,t.
    1460       execinf_stmt e m a1 t ->
    1461       execinf_stmt e m (Sfor a1 a2 a3 s) t
    1462   | execinf_Sfor_start_2: ∀e,m,s,a1,a2,a3,m1,t1,t2.
    1463       a1 <> Sskip ->
    1464       exec_stmt e m a1 t1 m1 Out_normal ->
    1465       execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 ->
    1466       execinf_stmt e m (Sfor a1 a2 a3 s) (t1 *** t2)
    1467   | execinf_Sfor_body: ∀e,m,s,a2,a3,v,t.
    1468       eval_expr e m a2 v ->
    1469       is_true v (typeof a2) ->
    1470       execinf_stmt e m s t ->
    1471       execinf_stmt e m (Sfor Sskip a2 a3 s) t
    1472   | execinf_Sfor_next: ∀e,m,s,a2,a3,v,m1,t1,t2,out1.
    1473       eval_expr e m a2 v ->
    1474       is_true v (typeof a2) ->
    1475       exec_stmt e m s t1 m1 out1 ->
    1476       out_normal_or_continue out1 ->
    1477       execinf_stmt e m1 a3 t2 ->
    1478       execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2)
    1479   | execinf_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,t1,t2,t3,out1.
    1480       eval_expr e m a2 v ->
    1481       is_true v (typeof a2) ->
    1482       exec_stmt e m s t1 m1 out1 ->
    1483       out_normal_or_continue out1 ->
    1484       exec_stmt e m1 a3 t2 m2 Out_normal ->
    1485       execinf_stmt e m2 (Sfor Sskip a2 a3 s) t3 ->
    1486       execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3)
    1487   | execinf_Sswitch:   ∀e,m,a,t,n,sl.
    1488       eval_expr e m a (Vint n) ->
    1489       execinf_stmt e m (seq_of_labeled_statement (select_switch n sl)) t ->
    1490       execinf_stmt e m (Sswitch a sl) t
    1491 
    1492 (** [evalinf_funcall ge m fd args t] holds if the invocation of function
    1493     [fd] on arguments [args] diverges, with observable trace [t]. *)
    1494 
    1495 with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
    1496   | evalinf_funcall_internal: ∀m,f,vargs,t,e,m1,m2.
    1497       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
    1498       bind_parameters e m1 f.(fn_params) vargs m2 ->
    1499       execinf_stmt e m2 f.(fn_body) t ->
    1500       evalinf_funcall m (Internal f) vargs t.
    1501 
    15021201End SEMANTICS.
    15031202*)
     1203
    15041204(* * * Whole-program semantics *)
    15051205
     
    15111211inductive initial_state (p: clight_program): state -> Prop :=
    15121212  | initial_state_intro: ∀b,f,ge,m0.
    1513       globalenv Genv ?? p = OK ? ge →
    1514       init_mem Genv ?? p = OK ? m0 →
     1213      globalenv Genv ?? (fst ??) p = OK ? ge →
     1214      init_mem Genv ?? (fst ??) p = OK ? m0 →
    15151215      find_symbol ?? ge (prog_main ?? p) = Some ? b →
    15161216      find_funct_ptr ?? ge b = Some ? f →
     
    15291229
    15301230definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    1531   ∀ge. globalenv ??? p = OK ? ge →
     1231  ∀ge. globalenv ??? (fst ??) p = OK ? ge →
    15321232  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
    1533 (*
    1534 (** Big-step execution of a whole program.  *)
    1535 
    1536 inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
    1537   | bigstep_program_terminates_intro: ∀b,f,m1,t,r.
    1538       let ge := Genv.globalenv p in
    1539       let m0 := Genv.init_mem p in
    1540       Genv.find_symbol ge p.(prog_main) = Some b ->
    1541       Genv.find_funct_ptr ge b = Some f ->
    1542       eval_funcall ge m0 f nil t m1 (Vint r) ->
    1543       bigstep_program_terminates p t r.
    1544 
    1545 inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
    1546   | bigstep_program_diverges_intro: ∀b,f,t.
    1547       let ge := Genv.globalenv p in
    1548       let m0 := Genv.init_mem p in
    1549       Genv.find_symbol ge p.(prog_main) = Some b ->
    1550       Genv.find_funct_ptr ge b = Some f ->
    1551       evalinf_funcall ge m0 f nil t ->
    1552       bigstep_program_diverges p t.
    1553 
    1554 (** * Implication from big-step semantics to transition semantics *)
    1555 
    1556 Section BIGSTEP_TO_TRANSITIONS.
    1557 
    1558 Variable prog: program.
    1559 Let ge : genv := Genv.globalenv prog.
    1560 
    1561 Definition exec_stmt_eval_funcall_ind
    1562   (PS: env -> mem -> statement -> trace -> mem -> outcome -> Prop)
    1563   (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) :=
    1564   fun a b c d e f g h i j k l m n o p q r s t u v w x y =>
    1565   conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y)
    1566        (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y).
    1567 
    1568 inductive outcome_state_match
    1569        (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop :=
    1570   | osm_normal:
    1571       outcome_state_match e m f k Out_normal (State f Sskip k e m)
    1572   | osm_break:
    1573       outcome_state_match e m f k Out_break (State f Sbreak k e m)
    1574   | osm_continue:
    1575       outcome_state_match e m f k Out_continue (State f Scontinue k e m)
    1576   | osm_return_none: ∀k'.
    1577       call_cont k' = call_cont k ->
    1578       outcome_state_match e m f k
    1579         (Out_return None) (State f (Sreturn None) k' e m)
    1580   | osm_return_some: ∀a,v,k'.
    1581       call_cont k' = call_cont k ->
    1582       eval_expr ge e m a v ->
    1583       outcome_state_match e m f k
    1584         (Out_return (Some v)) (State f (Sreturn (Some a)) k' e m).
    1585 
    1586 Lemma is_call_cont_call_cont:
    1587   ∀k. is_call_cont k -> call_cont k = k.
    1588 Proof.
    1589   destruct k; simpl; intros; contradiction || auto.
    1590 Qed.
    1591 
    1592 Lemma exec_stmt_eval_funcall_steps:
    1593   (∀e,m,s,t,m',out.
    1594    exec_stmt ge e m s t m' out ->
    1595    ∀f,k. exists S,
    1596    star step ge (State f s k e m) t S
    1597    /\ outcome_state_match e m' f k out S)
    1598 /\
    1599   (∀m,fd,args,t,m',res.
    1600    eval_funcall ge m fd args t m' res ->
    1601    ∀k.
    1602    is_call_cont k ->
    1603    star step ge (Callstate fd args k m) t (Returnstate res k m')).
    1604 Proof.
    1605   apply exec_stmt_eval_funcall_ind; intros.
    1606 
    1607 (* skip *)
    1608   econstructor; split. apply star_refl. constructor.
    1609 
    1610 (* assign *)
    1611   econstructor; split. apply star_one. econstructor; eauto. constructor.
    1612 
    1613 (* call none *)
    1614   econstructor; split.
    1615   eapply star_left. econstructor; eauto.
    1616   eapply star_right. apply H4. simpl; auto. econstructor. reflexivity. traceEq.
    1617   constructor.
    1618 
    1619 (* call some *)
    1620   econstructor; split.
    1621   eapply star_left. econstructor; eauto.
    1622   eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq.
    1623   constructor.
    1624 
    1625 (* sequence 2 *)
    1626   destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1.
    1627   destruct (H2 f k) as [S2 [A2 B2]].
    1628   econstructor; split.
    1629   eapply star_left. econstructor.
    1630   eapply star_trans. eexact A1.
    1631   eapply star_left. constructor. eexact A2.
    1632   reflexivity. reflexivity. traceEq.
    1633   auto.
    1634 
    1635 (* sequence 1 *)
    1636   destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]].
    1637   set (S2 :=
    1638     match out with
    1639     | Out_break => State f Sbreak k e m1
    1640     | Out_continue => State f Scontinue k e m1
    1641     | _ => S1
    1642     end).
    1643   exists S2; split.
    1644   eapply star_left. econstructor.
    1645   eapply star_trans. eexact A1.
    1646   unfold S2; inv B1.
    1647     congruence.
    1648     apply star_one. apply step_break_seq.
    1649     apply star_one. apply step_continue_seq.
    1650     apply star_refl.
    1651     apply star_refl.
    1652   reflexivity. traceEq.
    1653   unfold S2; inv B1; congruence || econstructor; eauto.
    1654 
    1655 (* ifthenelse true *)
    1656   destruct (H2 f k) as [S1 [A1 B1]].
    1657   exists S1; split.
    1658   eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq.
    1659   auto.
    1660 
    1661 (* ifthenelse false *)
    1662   destruct (H2 f k) as [S1 [A1 B1]].
    1663   exists S1; split.
    1664   eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq.
    1665   auto.
    1666 
    1667 (* return none *)
    1668   econstructor; split. apply star_refl. constructor. auto.
    1669 
    1670 (* return some *)
    1671   econstructor; split. apply star_refl. econstructor; eauto.
    1672 
    1673 (* break *)
    1674   econstructor; split. apply star_refl. constructor.
    1675 
    1676 (* continue *)
    1677   econstructor; split. apply star_refl. constructor.
    1678 
    1679 (* while false *)
    1680   econstructor; split.
    1681   apply star_one. eapply step_while_false; eauto.
    1682   constructor.
    1683 
    1684 (* while stop *)
    1685   destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
    1686   set (S2 :=
    1687     match out' with
    1688     | Out_break => State f Sskip k e m'
    1689     | _ => S1
    1690     end).
    1691   exists S2; split.
    1692   eapply star_left. eapply step_while_true; eauto.
    1693   eapply star_trans. eexact A1.
    1694   unfold S2. inversion H3; subst.
    1695   inv B1. apply star_one. constructor.   
    1696   apply star_refl.
    1697   reflexivity. traceEq.
    1698   unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
    1699 
    1700 (* while loop *)
    1701   destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
    1702   destruct (H5 f k) as [S2 [A2 B2]].
    1703   exists S2; split.
    1704   eapply star_left. eapply step_while_true; eauto.
    1705   eapply star_trans. eexact A1.
    1706   eapply star_left.
    1707   inv H3; inv B1; apply step_skip_or_continue_while; auto.
    1708   eexact A2.
    1709   reflexivity. reflexivity. traceEq.
    1710   auto.
    1711 
    1712 (* dowhile false *)
    1713   destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
    1714   exists (State f Sskip k e m1); split.
    1715   eapply star_left. constructor.
    1716   eapply star_right. eexact A1.
    1717   inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto.
    1718   reflexivity. traceEq.
    1719   constructor.
    1720 
    1721 (* dowhile stop *)
    1722   destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
    1723   set (S2 :=
    1724     match out1 with
    1725     | Out_break => State f Sskip k e m1
    1726     | _ => S1
    1727     end).
    1728   exists S2; split.
    1729   eapply star_left. apply step_dowhile.
    1730   eapply star_trans. eexact A1.
    1731   unfold S2. inversion H1; subst.
    1732   inv B1. apply star_one. constructor.
    1733   apply star_refl.
    1734   reflexivity. traceEq.
    1735   unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto.
    1736 
    1737 (* dowhile loop *)
    1738   destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
    1739   destruct (H5 f k) as [S2 [A2 B2]].
    1740   exists S2; split.
    1741   eapply star_left. apply step_dowhile.
    1742   eapply star_trans. eexact A1.
    1743   eapply star_left.
    1744   inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto.
    1745   eexact A2.
    1746   reflexivity. reflexivity. traceEq.
    1747   auto.
    1748 
    1749 (* for start *)
    1750   destruct (H1 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]. inv B1.
    1751   destruct (H3 f k) as [S2 [A2 B2]].
    1752   exists S2; split.
    1753   eapply star_left. apply step_for_start; auto.   
    1754   eapply star_trans. eexact A1.
    1755   eapply star_left. constructor. eexact A2.
    1756   reflexivity. reflexivity. traceEq.
    1757   auto.
    1758 
    1759 (* for false *)
    1760   econstructor; split.
    1761   eapply star_one. eapply step_for_false; eauto.
    1762   constructor.
    1763 
    1764 (* for stop *)
    1765   destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]].
    1766   set (S2 :=
    1767     match out1 with
    1768     | Out_break => State f Sskip k e m1
    1769     | _ => S1
    1770     end).
    1771   exists S2; split.
    1772   eapply star_left. eapply step_for_true; eauto.
    1773   eapply star_trans. eexact A1.
    1774   unfold S2. inversion H3; subst.
    1775   inv B1. apply star_one. constructor.
    1776   apply star_refl.
    1777   reflexivity. traceEq.
    1778   unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
    1779 
    1780 (* for loop *)
    1781   destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]].
    1782   destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2.
    1783   destruct (H7 f k) as [S3 [A3 B3]].
    1784   exists S3; split.
    1785   eapply star_left. eapply step_for_true; eauto.
    1786   eapply star_trans. eexact A1.
    1787   eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e m1).
    1788   inv H3; inv B1.
    1789   apply star_one. constructor. auto.
    1790   apply star_one. constructor. auto.
    1791   eapply star_trans. eexact A2.
    1792   eapply star_left. constructor.
    1793   eexact A3.
    1794   reflexivity. reflexivity. reflexivity. reflexivity. traceEq.
    1795   auto.
    1796 
    1797 (* switch *)
    1798   destruct (H1 f (Kswitch k)) as [S1 [A1 B1]].
    1799   set (S2 :=
    1800     match out with
    1801     | Out_normal => State f Sskip k e m1
    1802     | Out_break => State f Sskip k e m1
    1803     | Out_continue => State f Scontinue k e m1
    1804     | _ => S1
    1805     end).
    1806   exists S2; split.
    1807   eapply star_left. eapply step_switch; eauto.
    1808   eapply star_trans. eexact A1.
    1809   unfold S2; inv B1.
    1810     apply star_one. constructor. auto.
    1811     apply star_one. constructor. auto.
    1812     apply star_one. constructor.
    1813     apply star_refl.
    1814     apply star_refl.
    1815   reflexivity. traceEq.
    1816   unfold S2. inv B1; simpl; econstructor; eauto.
    1817 
    1818 (* call internal *)
    1819   destruct (H2 f k) as [S1 [A1 B1]].
    1820   eapply star_left. eapply step_internal_function; eauto.
    1821   eapply star_right. eexact A1.
    1822   inv B1; simpl in H3; try contradiction.
    1823   (* Out_normal *)
    1824   assert (fn_return f = Tvoid /\ vres = Vundef).
    1825     destruct (fn_return f); auto || contradiction.
    1826   destruct H5. subst vres. apply step_skip_call; auto.
    1827   (* Out_return None *)
    1828   assert (fn_return f = Tvoid /\ vres = Vundef).
    1829     destruct (fn_return f); auto || contradiction.
    1830   destruct H6. subst vres.
    1831   rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
    1832   apply step_return_0; auto.
    1833   (* Out_return Some *)
    1834   destruct H3. subst vres.
    1835   rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
    1836   eapply step_return_1; eauto.
    1837   reflexivity. traceEq.
    1838 
    1839 (* call external *)
    1840   apply star_one. apply step_external_function; auto.
    1841 Qed.
    1842 
    1843 Lemma exec_stmt_steps:
    1844    ∀e,m,s,t,m',out.
    1845    exec_stmt ge e m s t m' out ->
    1846    ∀f,k. exists S,
    1847    star step ge (State f s k e m) t S
    1848    /\ outcome_state_match e m' f k out S.
    1849 Proof (proj1 exec_stmt_eval_funcall_steps).
    1850 
    1851 Lemma eval_funcall_steps:
    1852    ∀m,fd,args,t,m',res.
    1853    eval_funcall ge m fd args t m' res ->
    1854    ∀k.
    1855    is_call_cont k ->
    1856    star step ge (Callstate fd args k m) t (Returnstate res k m').
    1857 Proof (proj2 exec_stmt_eval_funcall_steps).
    1858 
    1859 Definition order (x y: unit) := False.
    1860 
    1861 Lemma evalinf_funcall_forever:
    1862   ∀m,fd,args,T,k.
    1863   evalinf_funcall ge m fd args T ->
    1864   forever_N step order ge tt (Callstate fd args k m) T.
    1865 Proof.
    1866   cofix CIH_FUN.
    1867   assert (∀e,m,s,T,f,k.
    1868           execinf_stmt ge e m s T ->
    1869           forever_N step order ge tt (State f s k e m) T).
    1870   cofix CIH_STMT.
    1871   intros. inv H.
    1872 
    1873 (* call none *)
    1874   eapply forever_N_plus.
    1875   apply plus_one. eapply step_call_none; eauto.
    1876   apply CIH_FUN. eauto. traceEq.
    1877 (* call some *)
    1878   eapply forever_N_plus.
    1879   apply plus_one. eapply step_call_some; eauto.
    1880   apply CIH_FUN. eauto. traceEq.
    1881 
    1882 (* seq 1 *)
    1883   eapply forever_N_plus.
    1884   apply plus_one. econstructor.
    1885   apply CIH_STMT; eauto. traceEq.
    1886 (* seq 2 *)
    1887   destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]].
    1888   inv B1.
    1889   eapply forever_N_plus.
    1890   eapply plus_left. constructor. eapply star_trans. eexact A1.
    1891   apply star_one. constructor. reflexivity. reflexivity.
    1892   apply CIH_STMT; eauto. traceEq.
    1893 
    1894 (* ifthenelse true *)
    1895   eapply forever_N_plus.
    1896   apply plus_one. eapply step_ifthenelse_true; eauto.
    1897   apply CIH_STMT; eauto. traceEq.
    1898 (* ifthenelse false *)
    1899   eapply forever_N_plus.
    1900   apply plus_one. eapply step_ifthenelse_false; eauto.
    1901   apply CIH_STMT; eauto. traceEq.
    1902 
    1903 (* while body *)
    1904   eapply forever_N_plus.
    1905   eapply plus_one. eapply step_while_true; eauto.
    1906   apply CIH_STMT; eauto. traceEq.
    1907 (* while loop *)
    1908   destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]].
    1909   eapply forever_N_plus with (s2 := State f (Swhile a s0) k e m1).
    1910   eapply plus_left. eapply step_while_true; eauto.
    1911   eapply star_right. eexact A1.
    1912   inv H3; inv B1; apply step_skip_or_continue_while; auto.
    1913   reflexivity. reflexivity.
    1914   apply CIH_STMT; eauto. traceEq.
    1915 
    1916 (* dowhile body *)
    1917   eapply forever_N_plus.
    1918   eapply plus_one. eapply step_dowhile.
    1919   apply CIH_STMT; eauto.
    1920   traceEq.
    1921 
    1922 (* dowhile loop *)
    1923   destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]].
    1924   eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e m1).
    1925   eapply plus_left. eapply step_dowhile.
    1926   eapply star_right. eexact A1.
    1927   inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto.
    1928   reflexivity. reflexivity.
    1929   apply CIH_STMT. eauto.
    1930   traceEq.
    1931 
    1932 (* for start 1 *)
    1933   assert (a1 <> Sskip). red; intros; subst. inv H0.
    1934   eapply forever_N_plus.
    1935   eapply plus_one. apply step_for_start; auto.
    1936   apply CIH_STMT; eauto.
    1937   traceEq.
    1938 
    1939 (* for start 2 *)
    1940   destruct (exec_stmt_steps _ _ _ _ _ _ H1 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]].
    1941   inv B1.
    1942   eapply forever_N_plus.
    1943   eapply plus_left. eapply step_for_start; eauto.
    1944   eapply star_right. eexact A1.
    1945   apply step_skip_seq.
    1946   reflexivity. reflexivity.
    1947   apply CIH_STMT; eauto.
    1948   traceEq.
    1949 
    1950 (* for body *)
    1951   eapply forever_N_plus.
    1952   apply plus_one. eapply step_for_true; eauto.
    1953   apply CIH_STMT; eauto.
    1954   traceEq.
    1955 
    1956 (* for next *)
    1957   destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
    1958   eapply forever_N_plus.
    1959   eapply plus_left. eapply step_for_true; eauto.
    1960   eapply star_trans. eexact A1.
    1961   apply star_one.
    1962   inv H3; inv B1; apply step_skip_or_continue_for2; auto.
    1963   reflexivity. reflexivity.
    1964   apply CIH_STMT; eauto.
    1965   traceEq.
    1966 
    1967 (* for body *)
    1968   destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
    1969   destruct (exec_stmt_steps _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]].
    1970   inv B2.
    1971   eapply forever_N_plus.
    1972   eapply plus_left. eapply step_for_true; eauto.
    1973   eapply star_trans. eexact A1.
    1974   eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto.
    1975   eapply star_right. eexact A2.
    1976   constructor.
    1977   reflexivity. reflexivity. reflexivity. reflexivity. 
    1978   apply CIH_STMT; eauto.
    1979   traceEq.
    1980 
    1981 (* switch *)
    1982   eapply forever_N_plus.
    1983   eapply plus_one. eapply step_switch; eauto.
    1984   apply CIH_STMT; eauto.
    1985   traceEq.
    1986 
    1987 (* call internal *)
    1988   intros. inv H0.
    1989   eapply forever_N_plus.
    1990   eapply plus_one. econstructor; eauto.
    1991   apply H; eauto.
    1992   traceEq.
    1993 Qed.
    1994 
    1995 Theorem bigstep_program_terminates_exec:
    1996   ∀t,r. bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
    1997 Proof.
    1998   intros. inv H. unfold ge0, m0 in *.
    1999   econstructor.
    2000   econstructor. eauto. eauto.
    2001   apply eval_funcall_steps. eauto. red; auto.
    2002   econstructor.
    2003 Qed.
    2004 
    2005 Theorem bigstep_program_diverges_exec:
    2006   ∀T. bigstep_program_diverges prog T ->
    2007   exec_program prog (Reacts T) \/
    2008   exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T.
    2009 Proof.
    2010   intros. inv H.
    2011   set (st := Callstate f nil Kstop m0).
    2012   assert (forever step ge0 st T).
    2013     eapply forever_N_forever with (order := order).
    2014     red; intros. constructor; intros. red in H. elim H.
    2015     eapply evalinf_funcall_forever; eauto.
    2016   destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
    2017   as [A | [t [s' [T' [B [C D]]]]]].
    2018   left. econstructor. econstructor. eauto. eauto. auto.
    2019   right. exists t. split.
    2020   econstructor. econstructor; eauto. eauto. auto.
    2021   subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
    2022 Qed.
    2023 
    2024 End BIGSTEP_TO_TRANSITIONS.
    2025 
    2026 
    2027 
    2028 *)
    2029 
    20301233 
  • Deliverables/D3.3/id-lookup-branch/Clight/Csyntax.ma

    r961 r1153  
    318318  data.  See module [AST] for more details. *)
    319319
    320 definition clight_program : Type[0] ≝ program clight_fundef type.
     320definition clight_program : Type[0] ≝ program clight_fundef (list init_data × type).
    321321
    322322(* * * Operations over types *)
  • Deliverables/D3.3/id-lookup-branch/Clight/test/insertsort.c.ma

    r965 r1153  
    55   generate Init_null at the moment. *)
    66
    7 definition myprog := mk_program clight_fundef type
     7definition myprog := mk_program clight_fundef ((list init_data) × type)
    88  [〈ident_of_nat 0 (* insert *), CL_Internal (
    99     mk_function Tvoid [〈ident_of_nat 2, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ]
     
    167167  )〉]
    168168  (ident_of_nat 12)
    169   [〈〈〈ident_of_nat 15 (* l6 *),
    170      [(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ]〉,
    171      Any〉,
    172      (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
    173   〈〈〈ident_of_nat 16 (* l5 *),
    174     [(Init_int8 (repr I8 36)) ; (Init_space 3) ;
    175     (Init_addrof Any (ident_of_nat 15) 0)]〉, Any〉,
    176     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
    177   〈〈〈ident_of_nat 17 (* l4 *),
    178     [(Init_int8 (repr I8 136)) ; (Init_space 3) ;
    179     (Init_addrof Any (ident_of_nat 16) 0)]〉, Any〉,
    180     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
    181   〈〈〈ident_of_nat 18 (* l3 *),
    182     [(Init_int8 (repr I8 105)) ; (Init_space 3) ;
    183     (Init_addrof Any (ident_of_nat 17) 0)]〉, Any〉,
    184     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
    185   〈〈〈ident_of_nat 19 (* l2 *),
    186     [(Init_int8 (repr I8 234)) ; (Init_space 3) ;
    187     (Init_addrof Any (ident_of_nat 18) 0)]〉, Any〉,
    188     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
    189   〈〈〈ident_of_nat 20 (* l1 *),
    190     [(Init_int8 (repr I8 240)) ; (Init_space 3) ;
    191     (Init_addrof Any (ident_of_nat 19) 0)]〉, Any〉,
    192     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉;
    193   〈〈〈ident_of_nat 14 (* l0 *),
    194     [(Init_int8 (repr I8 102)) ; (Init_space 3) ;
    195     (Init_addrof Any (ident_of_nat 20) 0)]〉, Any〉,
    196     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉]
     169  [〈〈ident_of_nat 15 (* l6 *), Any〉,
     170    〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ],
     171     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
     172  〈〈ident_of_nat 16 (* l5 *), Any〉,
     173    〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ;
     174    (Init_addrof Any (ident_of_nat 15) 0)],
     175    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
     176  〈〈ident_of_nat 17 (* l4 *), Any〉,
     177    〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ;
     178    (Init_addrof Any (ident_of_nat 16) 0)],
     179    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
     180  〈〈ident_of_nat 18 (* l3 *), Any〉,
     181    〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ;
     182    (Init_addrof Any (ident_of_nat 17) 0)],
     183    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
     184  〈〈ident_of_nat 19 (* l2 *), Any〉,
     185   〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ;
     186    (Init_addrof Any (ident_of_nat 18) 0)],
     187    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
     188  〈〈ident_of_nat 20 (* l1 *), Any〉,
     189   〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ;
     190    (Init_addrof Any (ident_of_nat 19) 0)],
     191    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
     192  〈〈ident_of_nat 14 (* l0 *), Any〉,
     193    〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ;
     194    (Init_addrof Any (ident_of_nat 20) 0)],
     195    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉]
    197196.
    198197
  • Deliverables/D3.3/id-lookup-branch/Clight/test/search.c.ma

    r978 r1153  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef ((list init_data) × type)
    55  [〈ident_of_nat 0 (* search *), CL_Internal (
    66     mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
  • Deliverables/D3.3/id-lookup-branch/Clight/test/sum.c.ma

    r965 r1153  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef (list init_data × type)
    55  [〈ident_of_nat 0 (* main *), CL_Internal (
    66     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
     
    4848   )〉]
    4949  (ident_of_nat 0)
    50   [〈〈〈ident_of_nat 3 (* src *),
    51      [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
     50  [〈〈ident_of_nat 3 (* src *), Any〉,
     51     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
    5252     (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
    53      (Init_int8 (repr I8 4)) ]〉, Any〉,
    54      (Tarray Any (Tint I8 Unsigned ) 5)〉]
     53     (Init_int8 (repr I8 4)) ],
     54     (Tarray Any (Tint I8 Unsigned ) 5)〉]
    5555.
    5656
  • Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

    r1102 r1153  
    11031103λp.
    11041104  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
    1105   let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in
     1105  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
    11061106  let globals ≝ fun_globals @ var_globals in
    1107   transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
     1107  transform_partial_program2 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.
  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    r1102 r1153  
    5454] qed.
    5555
    56 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_inv s ≝
     56definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
    5757λvars. foldr ? (Σs:stmt. stmt_inv s)
    58   (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
     58  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
    5959% [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
    6060qed.
     
    102102] qed.
    103103
    104 definition empty_vars : list (ident × (list init_data) × region × unit) →
    105                         list (ident × (list init_data) × region × unit) ≝
    106 map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
    107                [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
    108               \snd (\fst v)〉,
    109               \snd v〉).
     104definition empty_vars : list (ident × region × (list init_data)) →
     105                        list (ident × region × nat) ≝
     106map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
     107              size_init_data_list (\snd v)〉).
    110108
    111 definition replace_init : Cminor_program → Cminor_program ≝
     109definition replace_init : Cminor_program → Cminor_noinit_program ≝
    112110λp.
    113111  mk_program ??
  • Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma

    r1135 r1153  
    466466definition make_initial_state : Cminor_program → res (genv × state) ≝
    467467λp.
    468   do ge ← globalenv Genv ?? p;
    469   do m ← init_mem Genv ?? p;
     468  do ge ← globalenv Genv ?? (λx.x) p;
     469  do m ← init_mem Genv ?? (λx.x) p;
    470470  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    471471  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     
    474474definition Cminor_fullexec : fullexec io_out io_in ≝
    475475  mk_fullexec … Cminor_exec ? make_initial_state.
     476
     477definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
     478λp.
     479  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     480  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
     481  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
     482  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     483  OK ? 〈ge, Callstate f (nil ?) m SStop〉.
     484
     485definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
     486  mk_fullexec … Cminor_exec ? make_initial_noinit_state.
  • Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

    r1104 r1153  
    151151}.
    152152
    153 definition Cminor_program ≝ program (fundef internal_function) unit.
     153(* We define two closely related versions of Cminor, the first with the original
     154   initialisation data for global variables, and the second where the code is
     155   responsible for initialisation and we only give the size of each variable. *)
     156
     157definition Cminor_program ≝ program (fundef internal_function) (list init_data).
     158
     159definition Cminor_noinit_program ≝ program (fundef internal_function) nat.
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1105 r1153  
    718718qed.
    719719
    720 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     720definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    721721transform_partial_program ???
    722722  (transf_partial_fundef ?? c2ra_function).
     
    724724include "Cminor/initialisation.ma".
    725725
    726 definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
    727 λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
     726definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     727λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

    r1109 r1153  
    2020  | ertl_st_pop: register → label → ertl_statement
    2121  | ertl_st_push: register → label → ertl_statement
     22  | ertl_st_addr: register → register → ident → label → ertl_statement
     23(* XXX: changed from O'Caml
    2224  | ertl_st_addr_h: register → ident → label → ertl_statement
    2325  | ertl_st_addr_l: register → ident → label → ertl_statement
     26*)
    2427  | ertl_st_int: register → Byte → label → ertl_statement
    2528  | ertl_st_move: register → register → label → ertl_statement
     29  | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
     30(* XXX: changed from O'Caml
    2631  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
    2732  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
     33*)
    2834  | ertl_st_op1: Op1 → register → register → label → ertl_statement
    2935  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
     
    3238  | ertl_st_load: register → register → register → label → ertl_statement
    3339  | ertl_st_store: register → register → register → label → ertl_statement
    34   | ertl_st_call_id: ident → Byte → label → ertl_statement
     40  | ertl_st_call_id: ident → nat → label → ertl_statement
    3541  | ertl_st_cond: register → label → label → ertl_statement
    3642  | ertl_st_return: ertl_statement.
  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma

    r1091 r1153  
    22include "ERTL/ERTLToLTLI.ma".
    33include "LTL/LTL.ma".
     4include "ERTL/spill.ma".
    45
    56definition translate_internal ≝
    67  λf.
    78  λint_fun: ertl_internal_function.
    8     mk_ltl_internal_function ?
    9       (ertl_if_luniverse int_fun)
    10       (ertl_if_runiverse int_fun)
    11       (ertl_if_stacksize int_fun)
    12       (ertl_if_graph int_fun)
    13       ?
    14       ?.
     9
     10  let fresh_label () = Label.Gen.fresh int_fun.ERTL.f_luniverse in
     11
     12  let add_graph lbl stmt = graph := Label.Map.add lbl stmt !graph in
     13
     14  let generate stmt =
     15    let l = fresh_label () in
     16    add_graph l stmt ;
     17    l in
     18
     19  (* Build an interference graph for this function, and color
     20     it. Define a function that allows consulting the coloring. *)
     21
     22  let module G = struct
     23    let liveafter, graph = Build.build int_fun
     24    let uses = Uses.examine_internal int_fun
     25    let verbose = false
     26    let () =
     27      if verbose then
     28        Printf.printf "Starting hardware register allocation for %s.\n" f
     29  end in
     30
     31  let module C = Coloring.Color (G) in
     32
     33  let lookup r =
     34    Interference.Vertex.Map.find (Interference.lookup G.graph r) C.coloring
     35  in
     36
     37  (* Restrict the interference graph to concern spilled vertices only,
     38     and color it again, this time using stack slots as colors. *)
     39
     40  let module H = struct
     41    let graph = Interference.droph (Interference.restrict G.graph (fun v ->
     42      match Interference.Vertex.Map.find v C.coloring with
     43      | Coloring.Spill ->
     44          true
     45      | Coloring.Color _ ->
     46          false
     47    ))
     48    let verbose = false
     49    let () =
     50      if verbose then
     51        Printf.printf "Starting stack slot allocation for %s.\n" f
     52  end in
     53
     54  let module S = Spill.Color (H) in
     55
     56  (* Define a new function that consults both colorings at once. *)
     57
     58  let lookup r =
     59    match lookup r with
     60    | Coloring.Spill ->
     61        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
     62    | Coloring.Color color ->
     63        ERTLToLTLI.Color color
     64  in
     65
     66  (* We are now ready to instantiate the functor that deals with the
     67     translation of instructions. The reason why we make this a
     68     separate functor is purely pedagogical. Smaller modules are
     69     easier to understand. *)
     70
     71  (* We add the additional stack size required for spilled register to the stack
     72     size previously required for the function: this is the final stack size
     73     required for the locals. *)
     74
     75  let locals = S.locals + int_fun.ERTL.f_stacksize in
     76
     77  (* The full stack size is then the size of the locals in the stack plus the
     78     size of the formal parameters of the function. *)
     79
     80  let stacksize = int_fun.ERTL.f_params + locals in
     81
     82  let module I = ERTLToLTLI.Make (struct
     83    let lookup = lookup
     84    let generate = generate
     85    let fresh_label = fresh_label
     86    let add_graph = add_graph
     87    let locals = locals
     88    let stacksize = stacksize
     89  end) in
     90
     91  (* Translate the instructions in the existing control flow graph.
     92     Pure instructions whose destination pseudo-register is dead are
     93     eliminated on the fly. *)
     94
     95  let () =
     96    Label.Map.iter (fun label stmt ->
     97      let stmt =
     98        match Liveness.eliminable (G.liveafter label) stmt with
     99        | Some successor ->
     100            LTL.St_skip successor
     101        | None ->
     102            I.translate_statement stmt
     103      in
     104      graph := Label.Map.add label stmt !graph
     105    ) int_fun.ERTL.f_graph
     106  in
     107
     108  (* Build a [LTL] function. *)
     109
     110  {
     111    LTL.f_luniverse = int_fun.ERTL.f_luniverse;
     112    LTL.f_stacksize = stacksize ;
     113    LTL.f_entry = int_fun.ERTL.f_entry;
     114    LTL.f_exit = int_fun.ERTL.f_exit;
     115    LTL.f_graph = !graph
     116  }
    15117
    16118definition translate_funct ≝
  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTLI.ma

    r1109 r1153  
    8383    [ decision_colour src_hwr ⇒
    8484      if eq_Register dest_hwr src_hwr then
    85         joint_st_sequential ? globals (joint_instr_skip globals) l
     85        joint_st_goto ? globals l
    8686      else
    8787        let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
     
    9494    | decision_spill src_off ⇒
    9595      if eq_bv ? dest_off src_off then
    96         joint_st_sequential ? globals (joint_instr_skip globals) l
     96        joint_st_goto ? globals l
    9797      else
    9898        let temp_hwr ≝ RegisterSST in
     
    106106  λl.
    107107  if eq_nat stacksize 0 then
    108     joint_st_sequential ? globals (joint_instr_skip globals) l
     108    joint_st_goto ? globals l
    109109  else
    110110    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     
    122122  λl.
    123123  if eq_nat stacksize 0 then
    124     joint_st_sequential ? globals (joint_instr_skip globals) l
     124    joint_st_goto ? globals l
    125125  else
    126126    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     
    135135  λstmt: ertl_statement.
    136136  match stmt with
    137   [ ertl_st_skip l ⇒ joint_st_sequential ? globals (joint_instr_skip globals) l
     137  [ ertl_st_skip l ⇒ joint_st_goto ? globals l
    138138  | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
    139139  | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
     
    155155    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
    156156    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    157       joint_st_sequential ? globals (joint_instr_skip globals) l
    158   | ertl_st_addr_h r x l ⇒
    159     let 〈hdw, l〉 ≝ write globals r l in
    160     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     157      joint_st_goto ? globals l
     158  | ertl_st_addr rl rh x l ⇒
     159    let 〈hdw1, l〉 ≝ write globals rh l in
     160    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
    161161    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
    162       joint_st_sequential ? globals (joint_instr_address globals x ?) l
    163   | ertl_st_addr_l r x l ⇒
    164     let 〈hdw, l〉 ≝ write globals r l in
    165     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     162    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
     163    let 〈hdw2, l〉 ≝ write globals rl l in
     164    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
    166165    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
    167166      joint_st_sequential ? globals (joint_instr_address globals x ?) l
     167(*  | ertl_st_addr_h r x l ⇒
     168    let 〈hdw, l〉 ≝ write globals r l in
     169    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     170    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
     171      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
     172  | ertl_st_addr_l r x l ⇒
     173    let 〈hdw, l〉 ≝ write globals r l in
     174    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     175    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
     176      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
     177*)
    168178  | ertl_st_int r i l ⇒
    169179    let 〈hdw, l〉 ≝ write globals r l in
    170180      joint_st_sequential ? globals (joint_instr_int globals hdw i) l
    171181  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
     182  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
     183    let 〈hdw, l〉 ≝ write globals destr1 l in
     184    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     185    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     186    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     187    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     188    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     189    let l ≝ generate globals (joint_st_goto ? globals l) in
     190    let 〈hdw, l〉 ≝ write globals destr2 l in
     191    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     192    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
     193    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     194    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     195    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     196    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     197      joint_st_goto ? globals l
     198(*
    172199  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
    173200    let 〈hdw, l〉 ≝ write globals destr l in
     
    177204    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    178205    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    179       joint_st_sequential ? globals (joint_instr_skip globals) l
     206      joint_st_goto ? globals l
    180207  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
    181208    let 〈hdw, l〉 ≝ write globals destr l in
     
    186213    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    187214    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    188       joint_st_sequential ? globals (joint_instr_skip globals) l
     215      joint_st_goto ? globals l
     216*)
    189217  | ertl_st_op1 op1 destr srcr l ⇒
    190218    let 〈hdw, l〉 ≝ write globals destr l in
     
    192220    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
    193221    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    194       joint_st_sequential ? globals (joint_instr_skip globals) l
     222      joint_st_goto ? globals l
    195223  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
    196224    let 〈hdw, l〉 ≝ write globals destr l in
     
    200228    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    201229    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    202       joint_st_sequential ? globals (joint_instr_skip globals) l
     230      joint_st_goto ? globals l
    203231  | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
    204232  | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
     
    213241    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    214242    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    215       joint_st_sequential ? globals (joint_instr_skip globals) l
     243      joint_st_goto ? globals l
    216244  | ertl_st_store addr1 addr2 srcr l ⇒
    217245    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
     
    225253    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
    226254    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    227       joint_st_sequential ? globals (joint_instr_skip globals) l
    228   | ertl_st_call_id f ignore l ⇒  joint_st_sequential ? globals (joint_instr_call_id globals f) l
     255      joint_st_goto ? globals l
     256  | ertl_st_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l
    229257  | ertl_st_cond srcr lbl_true lbl_false ⇒
    230258    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
    231259    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    232       joint_st_sequential ? globals (joint_instr_skip globals) l
     260      joint_st_goto ? globals l
    233261  | ertl_st_return ⇒ joint_st_return ? globals
    234262  ].
  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1109 r1153  
    1 include "utilities/Fix.ma".
    21include "ASM/Util.ma".
    32include "ERTL/ERTL.ma".
     
    3837  λs: ertl_statement.
    3938  match s with
    40   [ ertl_st_return _ ⇒ [ ]
     39  [ ertl_st_return ⇒ [ ]
    4140  | ertl_st_skip l ⇒ [ l ]
    4241  | ertl_st_comment c l ⇒ [ l ]
     
    5049  | ertl_st_push _ l ⇒ [ l ]
    5150  | ertl_st_pop _ l ⇒ [ l ]
    52   | ertl_st_addr_h _ _ l ⇒ [ l ]
    53   | ertl_st_addr_l _ _ l ⇒ [ l ]
     51  | ertl_st_addr _ _ _ l ⇒ [ l ]
    5452  | ertl_st_int _ _ l ⇒ [ l ]
    5553  | ertl_st_move _ _ l ⇒ [ l ]
    56   | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
    57   | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
     54  | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
    5855  | ertl_st_op1 _ _ _ l ⇒ [ l ]
    5956  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
     
    10097definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
    10198
     99record lattice_property_sig: Type[1] ≝
     100{
     101  lp_type      : Type[0];
     102  lp_property  : Type[0];
     103  lp_bottom    : lp_type;
     104  lp_psingleton: register → lp_type;
     105  lp_hsingleton: Register → lp_type;
     106  lp_join      : lp_type → lp_type → lp_type;
     107  lp_diff      : lp_type → lp_type → lp_type;
     108  lp_equal     : lp_type → lp_type → bool;
     109  lp_is_maximal: lp_type → bool
     110}.
     111
     112definition property ≝
     113  mk_lattice_property_sig
     114    ((list register) × (list Register))
     115    lattice_property
     116    lattice_bottom
     117    lattice_psingleton
     118    lattice_hsingleton
     119    lattice_join
     120    lattice_diff
     121    lattice_equal
     122    lattice_is_maximal.
     123
    102124definition defined: ertl_statement → register_lattice ≝
    103125  λs.
     
    109131  | ertl_st_store _ _ _ _ ⇒ lattice_bottom
    110132  | ertl_st_cond _ _ _ ⇒ lattice_bottom
    111   | ertl_st_return _ ⇒ lattice_bottom
     133  | ertl_st_return ⇒ lattice_bottom
    112134  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
    113135  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
     
    124146  | ertl_st_pop r _ ⇒ lattice_psingleton r
    125147  | ertl_st_int r _ _ ⇒ lattice_psingleton r
    126   | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
    127   | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
     148  | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    128149  | ertl_st_move r _ _ ⇒ lattice_psingleton r
    129   | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
    130   | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
     150  (* XXX: change from o'caml *)
     151  | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    131152  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
    132153  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
     
    156177  | ertl_st_frame_size _ _ ⇒ lattice_bottom
    157178  | ertl_st_pop _ _ ⇒ lattice_bottom
    158   | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
    159   | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
     179  | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
    160180  | ertl_st_int _ _ _ ⇒ lattice_bottom
    161181  | ertl_st_clear_carry _ ⇒ lattice_bottom
     
    163183    (* Reads the hardware registers that are used to pass parameters. *)
    164184  | ertl_st_call_id _ nparams _ ⇒
    165     〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
     185    〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
    166186  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
    167187  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
     
    177197    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    178198    ]
    179   | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    180   | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     199  | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2)
    181200  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    182201  | ertl_st_store r1 r2 r3 _ ⇒
     
    184203  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    185204  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    186   | ertl_st_return _ ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     205  | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
    187206  ].
    188207
     
    204223  | ertl_st_call_id _ _ _ ⇒ None ?
    205224  | ertl_st_cond _ _ _ ⇒ None ?
    206   | ertl_st_return _ ⇒ None ?
     225  | ertl_st_return ⇒ None ?
    207226  | ertl_st_get_hdw r _ l ⇒
    208227    if list_set_member register (eq_identifier ?) r pliveafter ∨
     
    223242    else
    224243      Some ? l
    225   | ertl_st_addr_h r _ l ⇒
    226     if list_set_member register (eq_identifier ?) r pliveafter ∨
    227        list_set_member Register eq_Register RegisterCarry hliveafter then
    228       None ?
    229     else
    230       Some ? l
    231   | ertl_st_addr_l r _ l ⇒
    232     if list_set_member register (eq_identifier ?) r pliveafter ∨
     244  | ertl_st_addr r1 r2 _ l ⇒
     245    if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     246       list_set_member register (eq_identifier ?) r2 pliveafter ∨
    233247       list_set_member Register eq_Register RegisterCarry hliveafter then
    234248      None ?
     
    241255    else
    242256      Some ? l
    243   | ertl_st_opaccs_a _ r _ _ l ⇒
    244     if list_set_member register (eq_identifier ?) r pliveafter ∨
    245        list_set_member Register eq_Register RegisterCarry hliveafter then
    246       None ?
    247     else
    248       Some ? l
    249   | ertl_st_opaccs_b _ r _ _ l ⇒
    250     if list_set_member register (eq_identifier ?) r pliveafter ∨
     257  | ertl_st_opaccs _ d1 d2 _ _ l ⇒
     258    if list_set_member register (eq_identifier ?) d1 pliveafter ∨
     259       list_set_member register (eq_identifier ?) d2 pliveafter ∨
    251260       list_set_member Register eq_Register RegisterCarry hliveafter then
    252261      None ?
     
    292301
    293302definition valuation ≝ label → register_lattice.
     303definition rhs ≝ valuation → lattice_property.
     304definition equations ≝ label → rhs.
     305
     306axiom fix_lfp: equations → valuation.
     307
     308definition livebefore ≝
     309  λint_fun.
     310  λlabel.
     311  λliveafter: valuation.
     312  match lookup ? ? (ertl_if_graph int_fun) label with
     313  [ None      ⇒ ?
     314  | Some stmt ⇒ statement_semantics stmt (liveafter label)
     315  ].
     316  cases not_implemented (* XXX *)
     317qed.
     318
     319definition liveafter ≝
     320  λint_fun.
     321  λlivebefore.
     322  λlabel.
     323  λliveafter: valuation.
     324  match lookup ? ? (ertl_if_graph int_fun) label with
     325  [ None      ⇒ ?
     326  | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     327      lattice_join (livebefore successor liveafter) accu)
     328      lattice_bottom (statement_successors stmt)
     329  ].
     330  cases not_implemented (* XXX *)
     331qed.
    294332
    295333definition analyse: ertl_internal_function → valuation ≝
    296334  λint_fun.
    297   let livebefore ≝ λlabel. λliveafter: valuation.
    298     match lookup ? ? (ertl_if_graph int_fun) label with
    299     [ None      ⇒ ?
    300     | Some stmt ⇒ statement_semantics stmt (liveafter label)
    301     ]
    302   in
    303   let liveafter ≝ λlabel. λliveafter: valuation.
    304     match lookup ? ? (ertl_if_graph int_fun) label with
    305     [ None      ⇒ ?
    306     | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
    307         lattice_join (livebefore successor liveafter) accu)
    308         lattice_bottom (statement_successors stmt)
    309     ]
    310   in ?.
     335    fix_lfp (liveafter int_fun (livebefore int_fun)).
  • Deliverables/D3.3/id-lookup-branch/LIN/JointLTLLIN.ma

    r1109 r1153  
    77
    88inductive joint_instruction (globals: list ident): Type[0] ≝
    9   | joint_instr_skip: joint_instruction globals
    109  | joint_instr_comment: String → joint_instruction globals
    1110  | joint_instr_cost_label: costlabel → joint_instruction globals
     
    2827inductive joint_statement (A: Type[0]) (globals: list ident): Type[0] ≝
    2928  | joint_st_sequential: joint_instruction globals → A → joint_statement A globals
     29  | joint_st_goto: label → joint_statement A globals
    3030  | joint_st_return: joint_statement A globals.
  • Deliverables/D3.3/id-lookup-branch/LIN/LINToASM.ma

    r757 r1153  
    3333    match instr with
    3434    [ joint_st_sequential instr' _ ⇒
    35         match instr' with
    36         [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    37         | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    38         | _ ⇒ set_empty ?
    39         ]
     35      match instr' with
     36      [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     37      | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     38      | _ ⇒ set_empty ?
     39      ]
     40    | joint_st_return ⇒ set_empty ?
    4041    | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    41     | joint_st_return ⇒ set_empty ?
    42     ] in
     42    ]
     43  in
    4344  match label with
    4445  [ None ⇒ generated
     
    8889  λstatement: pre_lin_statement globals_old.
    8990  match statement with
    90   [ joint_st_return ⇒ Instruction (RET ?)
    91   | joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
     91  [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
     92  | joint_st_return ⇒ Instruction (RET ?)
    9293  | joint_st_sequential instr _ ⇒
    93     match instr with
    94     [ joint_instr_comment comment ⇒ Comment comment
    95     | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
    96     | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
    97     | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
    98     | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    99     | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
    100     | joint_instr_opaccs accs ⇒
    101       match accs with
    102       [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    103       | Divu ⇒ Instruction (DIV ? ACC_A ACC_B)
    104       | Modu ⇒ ?
     94      match instr with
     95      [ joint_instr_comment comment ⇒ Comment comment
     96      | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
     97      | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
     98      | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
     99      | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
     100      | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
     101      | joint_instr_opaccs accs ⇒
     102        match accs with
     103        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
     104        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
     105        ]
     106      | joint_instr_op1 op1 ⇒
     107        match op1 with
     108        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
     109        | Inc ⇒ Instruction (INC ? ACC_A)
     110        ]
     111      | joint_instr_op2 op2 reg ⇒
     112        match op2 with
     113        [ Add ⇒
     114          let reg' ≝ register_address reg in
     115          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     116                                                         direct;
     117                                                         registr ]] x) → ? with
     118          [ ACC_A ⇒ λacc_a: True.
     119            Instruction (ADD ? ACC_A accumulator_address)
     120          | DIRECT d ⇒ λdirect1: True.
     121            Instruction (ADD ? ACC_A (DIRECT d))
     122          | REGISTER r ⇒ λregister1: True.
     123            Instruction (ADD ? ACC_A (REGISTER r))
     124          | _ ⇒ λother: False. ⊥
     125          ] (subaddressing_modein … reg')
     126        | Addc ⇒
     127          let reg' ≝ register_address reg in
     128          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     129                                                         direct;
     130                                                         registr ]] x) → ? with
     131          [ ACC_A ⇒ λacc_a: True.
     132            Instruction (ADDC ? ACC_A accumulator_address)
     133          | DIRECT d ⇒ λdirect2: True.
     134            Instruction (ADDC ? ACC_A (DIRECT d))
     135          | REGISTER r ⇒ λregister2: True.
     136            Instruction (ADDC ? ACC_A (REGISTER r))
     137          | _ ⇒ λother: False. ⊥
     138          ] (subaddressing_modein … reg')
     139        | Sub ⇒
     140          let reg' ≝ register_address reg in
     141          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     142                                                         direct;
     143                                                         registr ]] x) → ? with
     144          [ ACC_A ⇒ λacc_a: True.
     145            Instruction (SUBB ? ACC_A accumulator_address)
     146          | DIRECT d ⇒ λdirect3: True.
     147            Instruction (SUBB ? ACC_A (DIRECT d))
     148          | REGISTER r ⇒ λregister3: True.
     149            Instruction (SUBB ? ACC_A (REGISTER r))
     150          | _ ⇒ λother: False. ⊥
     151          ] (subaddressing_modein … reg')
     152        | And ⇒
     153          let reg' ≝ register_address reg in
     154          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     155                                                         direct;
     156                                                         registr ]] x) → ? with
     157          [ ACC_A ⇒ λacc_a: True.
     158            Instruction (NOP ?)
     159          | DIRECT d ⇒ λdirect4: True.
     160            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     161          | REGISTER r ⇒ λregister4: True.
     162            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     163          | _ ⇒ λother: False. ⊥
     164          ] (subaddressing_modein … reg')
     165        | Or ⇒
     166          let reg' ≝ register_address reg in
     167          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     168                                                         direct;
     169                                                         registr ]] x) → ? with
     170          [ ACC_A ⇒ λacc_a: True.
     171            Instruction (NOP ?)
     172          | DIRECT d ⇒ λdirect5: True.
     173            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     174          | REGISTER r ⇒ λregister5: True.
     175            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     176          | _ ⇒ λother: False. ⊥
     177          ] (subaddressing_modein … reg')
     178        | Xor ⇒
     179          let reg' ≝ register_address reg in
     180          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     181                                                         direct;
     182                                                         registr ]] x) → ? with
     183          [ ACC_A ⇒ λacc_a: True.
     184            Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
     185          | DIRECT d ⇒ λdirect6: True.
     186            Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
     187          | REGISTER r ⇒ λregister6: True.
     188            Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
     189          | _ ⇒ λother: False. ⊥
     190          ] (subaddressing_modein … reg')
     191        ]
     192      | joint_instr_int reg byte ⇒
     193        let reg' ≝ register_address reg in
     194          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     195                                                         direct;
     196                                                         registr ]] x) → ? with
     197          [ REGISTER r ⇒ λregister7: True.
     198            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
     199          | ACC_A ⇒ λacc: True.
     200            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
     201          | DIRECT d ⇒ λdirect7: True.
     202            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
     203          | _ ⇒ λother: False. ⊥
     204          ] (subaddressing_modein … reg')
     205      | joint_instr_from_acc reg ⇒
     206        let reg' ≝ register_address reg in
     207          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     208                                                         direct;
     209                                                         registr ]] x) → ? with
     210          [ REGISTER r ⇒ λregister8: True.
     211            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
     212          | ACC_A ⇒ λacc: True.
     213            Instruction (NOP ?)
     214          | DIRECT d ⇒ λdirect8: True.
     215            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
     216          | _ ⇒ λother: False. ⊥
     217          ] (subaddressing_modein … reg')
     218      | joint_instr_to_acc reg ⇒
     219        let reg' ≝ register_address reg in
     220          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     221                                                         direct;
     222                                                         registr ]] x) → ? with
     223          [ REGISTER r ⇒ λregister9: True.
     224            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
     225          | DIRECT d ⇒ λdirect9: True.
     226            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
     227          | ACC_A ⇒ λacc_a: True.
     228            Instruction (NOP ?)
     229          | _ ⇒ λother: False. ⊥
     230          ] (subaddressing_modein … reg')
     231      | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     232      | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     233      | joint_instr_address addr proof ⇒
     234        let look ≝ association addr globals (prf ? proof) in
     235          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
     236      | joint_instr_cond_acc lbl ⇒
     237        (* dpm: this should be handled in translate_code! *)
     238        Instruction (JNZ ? (word_of_identifier ? lbl))
     239      | joint_instr_set_carry ⇒
     240        Instruction (SETB ? CARRY)
    105241      ]
    106     | joint_instr_op1 op1 ⇒
    107       match op1 with
    108       [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    109       | Inc ⇒ Instruction (INC ? ACC_A)
    110       ]
    111     | joint_instr_op2 op2 reg ⇒
    112       match op2 with
    113       [ Add ⇒
    114         let reg' ≝ register_address (Register_of_register reg) in
    115         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    116                                                        direct;
    117                                                        registr ]] x) → ? with
    118         [ ACC_A ⇒ λacc_a: True.
    119           Instruction (ADD ? ACC_A accumulator_address)
    120         | DIRECT d ⇒ λdirect1: True.
    121           Instruction (ADD ? ACC_A (DIRECT d))
    122         | REGISTER r ⇒ λregister1: True.
    123           Instruction (ADD ? ACC_A (REGISTER r))
    124         | _ ⇒ λother: False. ⊥
    125         ] (subaddressing_modein … reg')
    126       | Addc ⇒
    127         let reg' ≝ register_address (Register_of_register reg) in
    128         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    129                                                        direct;
    130                                                        registr ]] x) → ? with
    131         [ ACC_A ⇒ λacc_a: True.
    132           Instruction (ADDC ? ACC_A accumulator_address)
    133         | DIRECT d ⇒ λdirect2: True.
    134           Instruction (ADDC ? ACC_A (DIRECT d))
    135         | REGISTER r ⇒ λregister2: True.
    136           Instruction (ADDC ? ACC_A (REGISTER r))
    137         | _ ⇒ λother: False. ⊥
    138         ] (subaddressing_modein … reg')
    139       | Sub ⇒
    140         let reg' ≝ register_address (Register_of_register reg) in
    141         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    142                                                        direct;
    143                                                        registr ]] x) → ? with
    144         [ ACC_A ⇒ λacc_a: True.
    145           Instruction (SUBB ? ACC_A accumulator_address)
    146         | DIRECT d ⇒ λdirect3: True.
    147           Instruction (SUBB ? ACC_A (DIRECT d))
    148         | REGISTER r ⇒ λregister3: True.
    149           Instruction (SUBB ? ACC_A (REGISTER r))
    150         | _ ⇒ λother: False. ⊥
    151         ] (subaddressing_modein … reg')
    152       | And ⇒
    153         let reg' ≝ register_address (Register_of_register reg) in
    154         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    155                                                        direct;
    156                                                        registr ]] x) → ? with
    157         [ ACC_A ⇒ λacc_a: True.
    158           Instruction (NOP ?)
    159         | DIRECT d ⇒ λdirect4: True.
    160           Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    161         | REGISTER r ⇒ λregister4: True.
    162           Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    163         | _ ⇒ λother: False. ⊥
    164         ] (subaddressing_modein … reg')
    165       | Or ⇒
    166         let reg' ≝ register_address (Register_of_register reg) in
    167         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    168                                                        direct;
    169                                                        registr ]] x) → ? with
    170         [ ACC_A ⇒ λacc_a: True.
    171           Instruction (NOP ?)
    172         | DIRECT d ⇒ λdirect5: True.
    173           Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    174         | REGISTER r ⇒ λregister5: True.
    175           Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    176         | _ ⇒ λother: False. ⊥
    177         ] (subaddressing_modein … reg')
    178       | Xor ⇒
    179         let reg' ≝ register_address (Register_of_register reg) in
    180         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    181                                                        direct;
    182                                                        registr ]] x) → ? with
    183         [ ACC_A ⇒ λacc_a: True.
    184           Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
    185         | DIRECT d ⇒ λdirect6: True.
    186           Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
    187         | REGISTER r ⇒ λregister6: True.
    188           Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
    189         | _ ⇒ λother: False. ⊥
    190         ] (subaddressing_modein … reg')
    191       ]
    192     | joint_instr_int reg byte ⇒
    193       let reg' ≝ register_address (Register_of_register reg) in
    194         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    195                                                        direct;
    196                                                        registr ]] x) → ? with
    197         [ REGISTER r ⇒ λregister7: True.
    198           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
    199         | ACC_A ⇒ λacc: True.
    200           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
    201         | DIRECT d ⇒ λdirect7: True.
    202           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
    203         | _ ⇒ λother: False. ⊥
    204         ] (subaddressing_modein … reg')
    205     | joint_instr_from_acc reg ⇒
    206       let reg' ≝ register_address (Register_of_register reg) in
    207         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    208                                                        direct;
    209                                                        registr ]] x) → ? with
    210         [ REGISTER r ⇒ λregister8: True.
    211           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
    212         | ACC_A ⇒ λacc: True.
    213           Instruction (NOP ?)
    214         | DIRECT d ⇒ λdirect8: True.
    215           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
    216         | _ ⇒ λother: False. ⊥
    217         ] (subaddressing_modein … reg')
    218     | joint_instr_to_acc reg ⇒
    219       let reg' ≝ register_address (Register_of_register reg) in
    220         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    221                                                        direct;
    222                                                        registr ]] x) → ? with
    223         [ REGISTER r ⇒ λregister9: True.
    224           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    225         | DIRECT d ⇒ λdirect9: True.
    226           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    227         | ACC_A ⇒ λacc_a: True.
    228           Instruction (NOP ?)
    229         | _ ⇒ λother: False. ⊥
    230         ] (subaddressing_modein … reg')
    231     | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    232     | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    233     | joint_instr_address addr proof ⇒
    234       let look ≝ association addr globals (prf ? proof) in
    235         Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    236     | joint_instr_cond_acc lbl ⇒
    237       (* dpm: this should be handled in translate_code! *)
    238       WithLabel (JNZ ? (word_of_identifier ? lbl))
    239     ]
    240   ].
     242    ].
    241243  try assumption
    242244  try @ I
     
    312314definition globals_addr_internal ≝
    313315  λres_offset.
    314   λx_size: Identifier × nat.
     316  λx_size: ident × nat.
    315317    let 〈res, offset〉 ≝ res_offset in
    316318    let 〈x, size〉 ≝ x_size in
  • Deliverables/D3.3/id-lookup-branch/LTL/LTLToLIN.ma

    r759 r1153  
    1212    [ joint_st_return ⇒ joint_st_return ? globals
    1313    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
    14     | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl
     14    | joint_st_goto l ⇒ joint_st_goto ? globals l
    1515    ].
    1616   
    17 definition require: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    18   λl: ident.
     17definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     18  λl: label.
    1919  λg: BitVectorTrieSet 16.
    2020    set_insert ? (word_of_identifier ? l) g.
    2121   
    22 definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    23   λl: ident.
     22definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     23  λl: label.
    2424  λg: BitVectorTrieSet 16.
    2525    set_insert ? (word_of_identifier ? l) g.
    2626   
    27 definition marked: ident → BitVectorTrieSet 16 → bool ≝
    28   λl: ident.
     27definition marked: label → BitVectorTrieSet 16 → bool ≝
     28  λl: label.
    2929  λg: BitVectorTrieSet 16.
    3030    set_member ? (word_of_identifier ? l) g.
     
    3434definition graph_lookup ≝
    3535  λglobals: list ident.
    36   λl: ident.
     36  λl: label.
    3737  λgr: ltl_statement_graph globals.
    3838    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
    3939   
    40 definition fetch: ∀globals: list ident. ident → ltl_statement_graph globals → option (ltl_statement globals) ≝
     40definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝
    4141  λglobals: list ident.
    42   λl: ident.
     42  λl: label.
    4343  λg: ltl_statement_graph globals.
    4444    graph_lookup globals l g.
     
    4747  λl2, visited, required, globals, generated, g, n.
    4848  λvisit:
    49   ∀globals: list Identifier.
    50   ∀g: LTLStatementGraph globals.
     49  ∀globals: list ident.
     50  ∀g: ltl_statement_graph globals.
    5151  ∀required: BitVectorTrieSet 16.
    5252  ∀visited: BitVectorTrieSet 16.
    53   ∀generated: list (PreLINStatement globals).
    54   ∀l: Identifier.
     53  ∀generated: list (pre_lin_statement globals).
     54  ∀l: label.
    5555  ∀n: nat.
    56     BitVectorTrieSet 16 × (list (PreLINStatement globals)).
     56    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    5757  if marked l2 visited then
    58     〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉
     58    〈require l2 required, (joint_st_goto ? globals l2) :: generated〉
    5959  else
    6060   visit globals g required visited generated l2 n.
    6161
    62 let rec visit (globals: list ident) (g: ltl_statement_graph globals)
    63               (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    64               (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
     62(* XXX: look at this.  way too complicated to understand whether it is correct,
     63   in my opinion.
     64*)
     65let rec visit
     66  (globals: list ident) (g: ltl_statement_graph globals)
     67  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
     68  (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
     69    on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝
    6570  match n with
    6671  [ O ⇒ 〈required, generated〉
     
    7681        match instr with
    7782        [ joint_instr_cond_acc l1 ⇒
     83              let required' ≝
     84                if marked l2 visited' then
     85                  require l2 required
     86                else
     87                  required in
     88              let 〈required', generated''〉 ≝
     89               foo l2 visited' required' globals generated'' g n' visit (*
     90                if marked l2 visited' then
     91                  〈required', (Joint_St_Goto ? globals l2) :: generated''〉
     92                else
     93                  visit globals g required' visited' generated'' l2 n'*) in
     94              let required'' ≝ require l1 required' in
     95                if ¬(marked l1 visited') then
     96                  visit globals g required'' visited' generated'' l1 n'
     97                else
     98                  〈required', generated''〉
     99          | _ ⇒
    78100            let required' ≝
    79101              if marked l2 visited' then
     
    81103              else
    82104                required in
    83             let 〈required', generated''〉 ≝
    84              foo l2 visited' required' globals generated'' g n' visit (*
    85               if marked l2 visited' then
    86                 〈required', (Joint_St_Goto ? globals l2) :: generated''〉
    87               else
    88                 visit globals g required' visited' generated'' l2 n'*) in
    89             let required'' ≝ require l1 required' in
    90               if ¬(marked l1 visited') then
    91                 visit globals g required'' visited' generated'' l1 n'
    92               else
    93                 〈required', generated''〉
    94         | _ ⇒
    95           let required' ≝
    96105            if marked l2 visited' then
    97               require l2 required
     106              〈required', joint_st_goto ? globals l2 :: generated''〉
    98107            else
    99               required in
    100           if marked l2 visited' then
    101             〈required', Joint_St_Goto ? globals l2 :: generated''〉
    102           else
    103             visit globals g required' visited' generated'' l2 n'
    104         ]
    105       | joint_st_goto lbl ⇒
    106         let required' ≝
    107           if marked lbl visited' then
    108             require lbl required
    109           else
    110             required in
    111         if marked lbl visited' then
    112           〈required', (Joint_St_Goto ? globals lbl) :: generated''〉
    113         else
    114           visit globals g required' visited' generated'' lbl n'
    115       | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    116       ]
     108              visit globals g required' visited' generated'' l2 n'
     109          ]
     110        | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     111    | joint_st_goto l ⇒
     112       let required' ≝
     113         if marked l visited' then
     114           require l required
     115         else
     116           required
     117       in
     118         if marked l visited' then
     119           〈required', joint_st_goto ? globals l :: generated''〉
     120         else
     121           visit globals g required' visited' generated'' l n'
    117122    ]
    118   ].
     123  ]
     124].
    119125
    120126(*
  • Deliverables/D3.3/id-lookup-branch/RTL/RTL.ma

    r1109 r1153  
    1010  | rtl_st_skip: label → rtl_statement
    1111  | rtl_st_cost: costlabel → label → rtl_statement
     12                (* ldest, hdest, symbol, next *)
    1213  | rtl_st_addr: register → register → ident → label → rtl_statement
     14                (* ldest, hdest, next *)
    1315  | rtl_st_stack_addr: register → register → label → rtl_statement
    1416  | rtl_st_int: register → Byte → label → rtl_statement
     17                (* dest, src, next *)
    1518  | rtl_st_move: register → register → label → rtl_statement
    1619  | rtl_st_clear_carry: label → rtl_statement
     20                (* op, acc dest, bacc dest, acc src, bacc src, next *)
    1721  | rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement
     22                (* op, dest, src, next *)
    1823  | rtl_st_op1: Op1 → register → register → label → rtl_statement
     24                (* op, dest, src1, src2, next *)
    1925  | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
    2026  | rtl_st_load: register → register → register → label → rtl_statement
  • Deliverables/D3.3/id-lookup-branch/RTL/RTLtoERTL.ma

    r1109 r1153  
    9797  | ertl_st_pop r _ ⇒ ertl_st_pop r l
    9898  | ertl_st_push r _ ⇒ ertl_st_push r l
    99   | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
    100   | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
     99  | ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l
    101100  | ertl_st_int r i _ ⇒ ertl_st_int r i l
    102101  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
    103   | ertl_st_opaccs_a opaccs d s1 s2 _ ⇒ ertl_st_opaccs_a opaccs d s1 s2 l
    104   | ertl_st_opaccs_b opaccs d s1 s2 _ ⇒ ertl_st_opaccs_b opaccs d s1 s2 l
     102  | ertl_st_opaccs opaccs d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 s1 s2 l
    105103  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
    106104  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
     
    224222  [ nil ⇒ [get_params_hdw_internal]
    225223  | _ ⇒
    226     let l ≝ zip_pottier ? ? params parameters in
     224    let l ≝ zip_pottier ? ? params RegisterParams in
    227225      save_hdws l
    228226  ].
     
    260258definition get_params ≝
    261259  λparams.
    262   let n ≝ min (length ? params) (length ? parameters) in
     260  let n ≝ min (length ? params) (length ? RegisterParams) in
    263261  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    264262  let hdw_params ≝ get_params_hdw hdw_params in
     
    396394  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
    397395  | _ ⇒
    398     let l ≝ zip_pottier ? ? params parameters in
     396    let l ≝ zip_pottier ? ? params RegisterParams in
    399397      restore_hdws l
    400398  ].
     
    436434definition set_params ≝
    437435  λparams.
    438   let n ≝ min (|params|) (|parameters|) in
     436  let n ≝ min (|params|) (|RegisterParams|) in
    439437  let hdw_stack_params ≝ split ? params n ? in
    440438  let hdw_params ≝ \fst hdw_stack_params in
     
    477475    add_translates (
    478476      set_params args @ [
    479       adds_graph [ ertl_st_call_id f (bitvector_of_nat ? nb_args) start_lbl ];
     477      adds_graph [ ertl_st_call_id f nb_args start_lbl ];
    480478      fetch_result ret_regs
    481479      ]
     
    489487  [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
    490488  | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
    491   | rtl_st_addr r1 r2 x lbl' ⇒
    492     adds_graph [
    493       ertl_st_addr_l r1 x lbl;
    494       ertl_st_addr_h r2 x lbl
    495     ] lbl lbl' def
     489  | rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def
    496490  | rtl_st_stack_addr r1 r2 lbl' ⇒
    497491    adds_graph [
     
    502496  | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
    503497  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
     498      add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
     499(* XXX: change from o'caml
    504500    adds_graph [
    505501      ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl;
    506502      ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl
    507503      ] lbl lbl' def
     504*)
    508505  | rtl_st_op1 op1 destr srcr lbl' ⇒
    509506    add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
     
    533530  λdef.
    534531  let nb_params ≝ |rtl_if_params def| in
    535   let added_stacksize ≝ max 0 (nb_params - |parameters|) in
     532  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
    536533  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
    537534  let entry' ≝ rtl_if_entry def in
     
    619616      | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    620617      | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    621       | ertl_st_addr_h _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    622       | ertl_st_addr_l _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     618      | ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    623619      | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    624620      | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    625       | ertl_st_opaccs_a _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    626       | ertl_st_opaccs_b _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     621      | ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    627622      | ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    628623      | ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
  • Deliverables/D3.3/id-lookup-branch/RTLabs/semantics.ma

    r961 r1153  
    168168    [ Internal fn ⇒
    169169        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
     170        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
     171           here *)
    170172        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    171173        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
     
    207209definition make_initial_state : RTLabs_program → res (genv × state) ≝
    208210λp.
    209   do ge ← globalenv Genv ?? p;
    210   do m ← init_mem Genv ?? p;
     211  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     212  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    211213  let main ≝ prog_main ?? p in
    212214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
  • Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma

    r1105 r1153  
    1414| St_cost : costlabel → label → statement
    1515| St_const : register → constant → label → statement
    16 | St_op1 : unary_operation → register → register → label → statement
    17 | St_op2 : binary_operation → register → register → register → label → statement
     16| St_op1 : unary_operation → register → register → label → statement (* destination source *)
     17| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
    1818| St_load : memory_chunk → register → register → label → statement
    1919| St_store : memory_chunk → register → register → label → statement
     
    7070
    7171(* Note that the global variables will be initialised by the code in main
    72    by this stage.  All initialisation data should only reserve space. *)
     72   by this stage, so the only initialisation data is the amount of space to
     73   allocate. *)
    7374
    74 definition RTLabs_program ≝ program (fundef internal_function) unit.
     75definition RTLabs_program ≝ program (fundef internal_function) nat.
    7576
    76 (* TO CONSIDER:
    77 
    78    - removing most successor labels from the statements (bit icky, what about
    79      return and jump tables?)
    80    - seems like load and store ought to have types that control the size of the
    81      register list based on the addressing mode; similarly, memory_chunk and
    82      register are probably related.
    83    - label and register generation really tell us something about the sets of
    84      labels and register that may appear, perhaps it should be renamed, or the
    85      graph made dependent on them to make it obvious, etc.
    86  *)
  • Deliverables/D3.3/id-lookup-branch/common/AST.ma

    r1064 r1153  
    282282  prog_funct: list (ident × F);
    283283  prog_main: ident;
    284   prog_vars: list (ident × (list init_data) × region × V)
     284  prog_vars: list (ident × region × V)
    285285}.
    286286
     
    290290
    291291definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
    292   map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
     292  map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ?? p).
    293293
    294294(* * * Generic transformations over programs *)
  • Deliverables/D3.3/id-lookup-branch/common/Errors.ma

    r1102 r1153  
    162162  constructor. auto. auto.
    163163Qed.
    164 
     164*)
     165
     166(* A monadic fold_left2 *)
     167
     168axiom WrongLength: String.
     169
     170let rec mfold_left2
     171  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
     172  (left: list B) (right: list C) on left: res A ≝
     173  match left with
     174  [ nil ⇒
     175    match right with
     176    [ nil ⇒ accu
     177    | cons hd tl ⇒ Error ? (msg WrongLength)
     178    ]
     179  | cons hd tl ⇒
     180    match right with
     181    [ nil ⇒ Error ? (msg WrongLength)
     182    | cons hd' tl' ⇒
     183       do accu ← accu;
     184       mfold_left2 … f (f accu hd hd') tl tl'
     185    ]
     186  ].
     187
     188(*
    165189(** * Reasoning over monadic computations *)
    166190
  • Deliverables/D3.3/id-lookup-branch/common/Globalenvs.ma

    r961 r1153  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type[0]. program F V → res (genv_t F);
     54  globalenv: ∀F,V: Type[0]. (V → list init_data) → program F V → res (genv_t F);
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type[0]. program F V → res mem;
     57  init_mem: ∀F,V: Type[0]. (V → list init_data) → program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
     
    486486
    487487definition add_globals : ∀F,V:Type[0].
    488        genv F × mem → list (ident × (list init_data) × region × V) →
     488       (V → (list init_data)) →
     489       genv F × mem → list (ident × region × V) →
    489490       res (genv F × mem) ≝
    490 λF,V,init_env,vars.
     491λF,V,extract_init,init_env,vars.
    491492  foldl ??
    492     (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V.
    493       match id_init with [ pair id_init1 info ⇒
    494       match id_init1 with [ pair id_init2 r ⇒
    495       match id_init2 with [ pair id init ⇒
     493    (λg_st: res (genv F × mem). λid_init: ident × region × V.
     494      let 〈id, r, init_info〉 ≝ id_init in
     495      let init ≝ extract_init init_info in
    496496        do 〈g,st〉 ← g_st;
    497497        match alloc_init_data st init r with [ pair st' b ⇒
     
    499499          do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    500500            OK ? 〈g', st''〉
    501         ] ] ] ])
     501        ] )
    502502    (OK ? init_env) vars.
    503503
    504 definition globalenv_initmem : ∀F,V:Type[0]. program F V → res (genv F × mem) ≝
    505 λF,V,p.
    506   add_globals F V
    507    〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
     504definition globalenv_initmem : ∀F,V:Type[0]. (V → (list init_data)) → program F V → res (genv F × mem) ≝
     505λF,V,init_info,p.
     506  add_globals F V init_info
     507   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
    508508   (prog_vars ?? p).
    509509
    510 definition globalenv_ : ∀F,V:Type[0]. program F V → res (genv F) ≝
    511 λF,V,p.
    512   do 〈g,m〉 ← globalenv_initmem F V p;
     510definition globalenv_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (genv F) ≝
     511λF,V,i,p.
     512  do 〈g,m〉 ← globalenv_initmem F V i p;
    513513    OK ? g.
    514 definition init_mem_ : ∀F,V:Type[0]. program F V → res (mem) ≝
    515 λF,V,p.
    516   do 〈g,m〉 ← globalenv_initmem F V p;
     514definition init_mem_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (mem) ≝
     515λF,V,i,p.
     516  do 〈g,m〉 ← globalenv_initmem F V i p;
    517517    OK ? m.
    518518
  • Deliverables/D3.3/id-lookup-branch/common/Registers.ma

    r1049 r1153  
    1616
    1717axiom register_ord: register → register → order.
    18 
    19 (* dpm: fix the Register/register mismatch *)
    20 axiom Register_of_register: register → Register.
    21 axiom register_of_Register: Register → register.
Note: See TracChangeset for help on using the changeset viewer.