Changeset 1153 for Deliverables/D3.3/idlookupbranch/Clight/Csem.ma
 Timestamp:
 Aug 30, 2011, 6:55:12 PM (8 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch
 Property svn:mergeinfo changed
/src merged: 11101132,11361150
 Property svn:mergeinfo changed

Deliverables/D3.3/idlookupbranch/Clight/Csem.ma
r1058 r1153 1197 1197 step ge (State f (Scost lbl s) k e m) 1198 1198 (Echarge lbl) (State f s k e m). 1199 1199 1200 (* 1200 (** * Alternate bigstep semantics *)1201 1202 (** ** Bigstep semantics for terminating statements and functions *)1203 1204 (** The execution of a statement produces an ``outcome'', indicating1205 how the execution terminated: either normally or prematurely1206 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_normal1216  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_normal1220  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 with1225  Out_break => Out_normal1226  o => o1227 end.1228 1229 Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=1230 match out, t with1231  Out_normal, Tvoid => v = Vundef1232  Out_return None, Tvoid => v = Vundef1233  Out_return (Some v'), ty => ty <> Tvoid /\ v'=v1234  _, _ => False1235 end.1236 1237 (** [exec_stmt ge e m1 s t m2 out] describes the execution of1238 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 this1241 evaluation. *)1242 1243 inductive exec_stmt: env > mem > statement > trace > mem > outcome > Prop :=1244  exec_Sskip: ∀e,m.1245 exec_stmt e m Sskip1246 E0 m Out_normal1247  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_normal1253  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_normal1261  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_normal1271  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 out1276  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 out1281  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' out1287  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' out1293  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 Sbreak1302 E0 m Out_break1303  exec_Scontinue: ∀e,m.1304 exec_stmt e m Scontinue1305 E0 m Out_continue1306  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_normal1311  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' out1318  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 out1326  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_normal1333  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 out1338  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 out1346  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 out1352  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_normal1357  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 out1364  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 out1373  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 of1380 function [fd] with arguments [args]. [res] is the value returned1381 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)) vres1390  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 Prop1395 with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.1396 1397 (** ** Bigstep 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 infinite1402 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) t1412  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) t1420  execinf_Sseq_1: ∀e,m,s1,s2,t.1421 execinf_stmt e m s1 t >1422 execinf_stmt e m (Ssequence s1 s2) t1423  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) t1432  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) t1437  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) t1442  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) t1452  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) t1462  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) t1472  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) t1491 1492 (** [evalinf_funcall ge m fd args t] holds if the invocation of function1493 [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 1502 1201 End SEMANTICS. 1503 1202 *) 1203 1504 1204 (* * * Wholeprogram semantics *) 1505 1205 … … 1511 1211 inductive initial_state (p: clight_program): state > Prop := 1512 1212  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 → 1515 1215 find_symbol ?? ge (prog_main ?? p) = Some ? b → 1516 1216 find_funct_ptr ?? ge b = Some ? f → … … 1529 1229 1530 1230 definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh. 1531 ∀ge. globalenv ??? p = OK ? ge →1231 ∀ge. globalenv ??? (fst ??) p = OK ? ge → 1532 1232 program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh. 1533 (*1534 (** Bigstep 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 in1539 let m0 := Genv.init_mem p in1540 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 in1548 let m0 := Genv.init_mem p in1549 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 bigstep 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_ind1562 (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_match1569 (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 k1579 (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 k1584 (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 S1597 /\ 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 with1639  Out_break => State f Sbreak k e m11640  Out_continue => State f Scontinue k e m11641  _ => S11642 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' with1688  Out_break => State f Sskip k e m'1689  _ => S11690 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 with1725  Out_break => State f Sskip k e m11726  _ => S11727 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 with1768  Out_break => State f Sskip k e m11769  _ => S11770 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 with1801  Out_normal => State f Sskip k e m11802  Out_break => State f Sskip k e m11803  Out_continue => State f Scontinue k e m11804  _ => S11805 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 S1848 /\ 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 2030 1233
Note: See TracChangeset
for help on using the changeset viewer.