Changeset 1147


Ignore:
Timestamp:
Aug 30, 2011, 4:09:20 PM (8 years ago)
Author:
campbell
Message:

Remove some obsolete commented out code, update a couple of comments.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1139 r1147  
    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) ≝
     
    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  ]
  • src/Clight/Csem.ma

    r1139 r1147  
    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
     
    15311231  ∀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 
  • src/Cminor/syntax.ma

    r1139 r1147  
    4141}.
    4242
     43(* We define two closely related versions of Cminor, the first with the original
     44   initialisation data for global variables, and the second where the code is
     45   responsible for initialisation and we only give the size of each variable. *)
     46
    4347definition Cminor_program ≝ program (fundef internal_function) (list init_data).
    4448
  • src/RTLabs/syntax.ma

    r1139 r1147  
    4545definition RTLabs_program ≝ program (fundef internal_function) nat.
    4646
    47 (* TO CONSIDER:
    48 
    49    - removing most successor labels from the statements (bit icky, what about
    50      return and jump tables?)
    51    - seems like load and store ought to have types that control the size of the
    52      register list based on the addressing mode; similarly, memory_chunk and
    53      register are probably related.
    54    - label and register generation really tell us something about the sets of
    55      labels and register that may appear, perhaps it should be renamed, or the
    56      graph made dependent on them to make it obvious, etc.
    57  *)
Note: See TracChangeset for help on using the changeset viewer.