analysis with Abst_same

3 files changed, 39 insertions, 22 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index bcdebca7..8cfbaaa1 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -127,6 +127,9 @@ End RELATION.
 Module RB := ADD_BOTTOM(RELATION).
 Module DS := Dataflow_Solver(RB)(NodeSetForward).
 
+Inductive abst_insn_out :=
+| Abst_same : RB.t -> abst_insn_out.
+
 Inductive sym_op : Type :=
 | SOp : operation -> sym_op
 | SLoad : memory_chunk -> addressing -> sym_op.
@@ -461,27 +464,27 @@ Section OPERATIONS.
     | _ => rel
     end.
 
-  Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t :=
+  Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : abst_insn_out :=
   match instr with
   | Inop _
   | Icond _ _ _ _ _
-  | Ijumptable _ _ => Some rel
+  | Ijumptable _ _ => Abst_same (Some rel)
   | Istore chunk addr args src _ =>
-    Some (store tenv chunk addr args src rel)
-  | Iop op args dst _ => Some (oper dst (SOp op) args rel)
-  | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel)
-  | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
-  | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel))
-  | Itailcall _ _ _ | Ireturn _ => RB.bot
+    Abst_same (Some (store tenv chunk addr args src rel))
+  | Iop op args dst _ => Abst_same (Some (oper dst (SOp op) args rel))
+  | Iload trap chunk addr args dst _ => Abst_same (Some (oper dst (SLoad chunk addr) args rel))
+  | Icall _ _ _ dst _ => Abst_same (Some (kill_reg dst (kill_mem rel)))
+  | Ibuiltin ef _ res _ => Abst_same (Some (kill_builtin_res res (apply_external_call ef rel)))
+  | Itailcall _ _ _ | Ireturn _ => Abst_same RB.bot
   end.
   End PER_NODE.
 
-Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t :=
+Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : abst_insn_out :=
   match ro with
-  | None => None
+  | None => Abst_same RB.bot
   | Some x =>
     match code ! pc with
-    | None => RB.bot
+    | None => Abst_same RB.bot
     | Some instr => apply_instr pc tenv instr x
     end
   end.
@@ -504,10 +507,12 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva
          match PMap.get pc inv with
          | None => true
          | Some rel =>
-           let rel' := apply_instr pc tenv instr rel in
-           List.forallb
-             (fun pc' => relb_leb rel' (PMap.get pc' inv))
-             (RTL.successors_instr instr)
+           match apply_instr pc tenv instr rel with
+           | Abst_same rel' =>
+             List.forallb
+               (fun pc' => relb_leb rel' (PMap.get pc' inv))
+               (RTL.successors_instr instr)
+           end
          end).
 (* No longer used. Incompatible with transfer functions that yield a different result depending on the successor.
 
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 7e456748..10ffe760 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -1298,7 +1298,10 @@ Section SOUNDNESS.
         PTree.get pc (fn_code fn) = Some instr ->
         In pc' (successors_instr instr) ->
         RB.ge (PMap.get pc' inv)
-              (apply_instr' (ctx:=ctx) tenv (fn_code fn) pc (PMap.get pc inv)).
+              (match apply_instr' (ctx:=ctx) tenv (fn_code fn) pc
+                                  (PMap.get pc inv) with
+               | Abst_same rel' => rel'
+              end).
 
     Definition is_inductive_allstep :=
       forall pc pc', is_inductive_step pc pc'.
@@ -1317,11 +1320,14 @@ Section SOUNDNESS.
       pose proof (ALL INSTR) as AT_PC.
       destruct (inv # pc).
       2: apply RB.ge_bot.
-      rewrite List.forallb_forall in AT_PC.
       unfold apply_instr'.
       rewrite INSTR.
-      apply relb_leb_correct.
-      auto.
+      destruct apply_instr.
+      { (* same *)
+        rewrite List.forallb_forall in AT_PC.
+        apply relb_leb_correct.
+        auto.
+      }
     Qed.
     
     Lemma checked_is_inductive_entry:
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 7af62b95..9a55f529 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -449,6 +449,7 @@ Lemma step_simulation:
               exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
 Proof.
   induction 1; intros S1' MS; inv MS.
+  all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))).
   - (* Inop *)
     exists (State ts tf sp pc' rs m). split.
     + apply exec_Inop; auto.
@@ -779,9 +780,14 @@ Proof.
          cbn in IND.
          rewrite H in IND.
          assert (RB.ge (fst (preanalysis tenv f)) # (if b then ifso else ifnot)
-          match (fst (preanalysis tenv f)) # pc with
-          | Some x => apply_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc tenv (Icond cond args ifso ifnot predb) x
-          | None => None
+          match
+            match (fst (preanalysis tenv f)) # pc with
+            | Some x =>
+                apply_instr (ctx:=ctx) pc tenv (Icond cond args ifso ifnot predb) x
+            | None => Abst_same RB.bot
+            end
+          with
+          | Abst_same rel' => rel'
           end) as INDUCTIVE by (destruct b; intuition).
          clear IND.