analysis with Abst_same

1 files changed, 20 insertions, 15 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.