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:
2 edited

Legend:

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

  • 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 
Note: See TracChangeset for help on using the changeset viewer.