diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-20 18:34:46 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-20 18:34:46 +0200 |
| commit | d858606e8400e6aab627f4aac5ec33ce9c2c80fe (patch) | |
| tree | bcf193357cdaf9ee6a09fe36a4c9a0cb042c617a /scheduling/BTLtoRTLproof.v | |
| parent | 8dc70c68f241e1397f2c65981202742fb0ff75a3 (diff) | |
| download | compcert-kvx-d858606e8400e6aab627f4aac5ec33ce9c2c80fe.tar.gz compcert-kvx-d858606e8400e6aab627f4aac5ec33ce9c2c80fe.zip | |
defines fsem (aka functional semantics) of BTL
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 08a77ae4..bbb984c4 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -292,7 +292,7 @@ Qed. Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s (STACKS : list_forall2 match_stackframes stack stack') (TRANSF : match_function dupmap f f') - (FS : final_step ge stack f sp rs1 m1 fin t s) + (FS : final_step tid ge stack f sp rs1 m1 fin t s) (i : instruction) (ATpc1 : (RTL.fn_code f') ! pc1 = Some i) (MF : match_final_inst dupmap fin i) @@ -338,7 +338,7 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi (TRANSF: match_function dupmap f f') (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin)) (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None) - (FS : final_step ge stack f sp rs1 m1 fin t s) + (FS : final_step tid ge stack f sp rs1 m1 fin t s) : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'. Proof. intros; exploit iblock_istep_simulation; eauto. @@ -359,7 +359,7 @@ Proof. Qed. Theorem plus_simulation s1 t s1': - step ge s1 t s1' -> + step tid ge s1 t s1' -> forall s2 (MS: match_states s1 s2), exists s2', plus RTL.step tge s2 t s2' |