cleaner symbolic semantic of load traps

1 files changed, 10 insertions, 12 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 033ed843..55afc19a 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -84,19 +84,17 @@ Fixpoint eval_sval ctx (sv: sval): option val :=
      SOME args <- eval_list_sval ctx l IN
      eval_operation (cge ctx) (csp ctx) op args (cm0 ctx)
   | Sload sm trap chunk addr lsv _ =>
+      SOME args <- eval_list_sval ctx lsv IN
+      SOME m <- eval_smem ctx sm IN
       match trap with
       | TRAP =>
-          SOME args <- eval_list_sval ctx lsv IN
           SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
-          SOME m <- eval_smem ctx sm IN
           Mem.loadv chunk m a
       | NOTRAP =>
-          SOME args <- eval_list_sval ctx lsv IN
-          match (eval_addressing (cge ctx) (csp ctx) addr args) with
+          match eval_addressing (cge ctx) (csp ctx) addr args with
           | None => Some Vundef
           | Some a =>
-              SOME m <- eval_smem ctx sm IN
-              match (Mem.loadv chunk m a) with
+              match Mem.loadv chunk m a with
               | None => Some Vundef
               | Some val => Some val
               end
@@ -641,7 +639,7 @@ Proof.
   - simpl. destruct SIS as (PRE&MEM&REG).
     rewrite Regmap.gss; simpl; auto.
     erewrite eval_list_sval_inj; simpl; auto.
-    autodestruct; rewrite MEM, LOAD; auto.
+    rewrite MEM; simpl. autodestruct. rewrite LOAD; auto.
 Qed.
 
 Definition sexec_store chunk addr args src sis: sistate :=
@@ -1004,7 +1002,7 @@ Proof.
   eapply set_sreg_abort; eauto.
   simpl. destruct SIS as (PRE&MEM&REG).
   erewrite eval_list_sval_inj; simpl; auto.
-  intros; autodestruct; try_simplify_someHyps.
+  rewrite MEM; simpl; autodestruct; try_simplify_someHyps.
 Qed.
 
 Lemma set_smem_abort ctx sm sis rs m:
@@ -1241,10 +1239,10 @@ Proof.
                                    (P1 := fun sm => eval_smem (bctx1 ctx) sm = eval_smem (bctx2 ctx) sm); simpl; auto.
   + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto.
     erewrite eval_operation_preserved; eauto.
-  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
-    erewrite eval_addressing_preserved;  eauto.
-    destruct (eval_addressing _ _ _ _); auto.
-    rewrite IHsv; auto.
+  + rewrite IHsv0; clear IHsv0. 
+    autodestruct; intros.
+    erewrite IHsv; do 2 autodestruct;
+    erewrite eval_addressing_preserved; eauto.
   + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto.
     rewrite IHsv0; auto.
   + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.