Changeset 1147
 Timestamp:
 Aug 30, 2011, 4:09:20 PM (8 years ago)
 Location:
 src
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Cexec.ma
r1139 r1147 7 7 include "Clight/TypeComparison.ma". 8 8 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) with18 [ None ⇒ λe1.?19  Some b ⇒ λe1.(match b return λb'.b=b' → ? with20 [ 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_inject37 on a:option (res ?) to res (Sig ? ?).38 coercion err_eject : ∀A.∀P:A → Prop.∀c:res (Sig A P).res A ≝ err_eject39 on _c:res (Sig ? ?) to res ?.40 coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject41 on _c:Sig ? ? to ?.42 *)43 9 definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝ 44 10 λA,P,a. match a with [ Error _ ⇒ True  OK v ⇒ P v ]. … … 181 147 λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ]. 182 148 183 (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with184 a structurally smaller value, we break out the surrounding Expr constructor185 and use exec_lvalue'. *)186 187 149 axiom BadlyTypedTerm : String. 188 150 axiom UnknownIdentifier : String. … … 190 152 axiom FailedLoad : String. 191 153 axiom 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'. *) 192 158 193 159 let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝ … … 584 550  S n' ⇒ 585 551 ! 〈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'; 597 553 ret ? 〈t ⧺ t',s''〉 598 554 ] 
src/Clight/Csem.ma
r1139 r1147 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 … … 1531 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 
src/Cminor/syntax.ma
r1139 r1147 41 41 }. 42 42 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 43 47 definition Cminor_program ≝ program (fundef internal_function) (list init_data). 44 48 
src/RTLabs/syntax.ma
r1139 r1147 45 45 definition RTLabs_program ≝ program (fundef internal_function) nat. 46 46 47 (* TO CONSIDER:48 49  removing most successor labels from the statements (bit icky, what about50 return and jump tables?)51  seems like load and store ought to have types that control the size of the52 register list based on the addressing mode; similarly, memory_chunk and53 register are probably related.54  label and register generation really tell us something about the sets of55 labels and register that may appear, perhaps it should be renamed, or the56 graph made dependent on them to make it obvious, etc.57 *)
Note: See TracChangeset
for help on using the changeset viewer.