progress moving to list of items

1 files changed, 23 insertions, 27 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 8cfbaaa1..46ae4aea 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -127,9 +127,6 @@ 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.
@@ -464,28 +461,29 @@ Section OPERATIONS.
     | _ => rel
     end.
 
-  Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : abst_insn_out :=
+  Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) :=
   match instr with
-  | Inop _
-  | Icond _ _ _ _ _
-  | Ijumptable _ _ => Abst_same (Some rel)
-  | Istore chunk addr args src _ =>
-    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
+  | Inop pc' => (pc', (Some rel))::nil
+  | Icond _ _ ifso ifnot _ => (ifso, (Some rel))::(ifnot, (Some rel))::nil
+  | Ijumptable _ targets => List.map (fun pc' => (pc', (Some rel))) targets
+  | Istore chunk addr args src pc' =>
+    (pc', (Some (store tenv chunk addr args src rel)))::nil
+  | Iop op args dst pc' => (pc', (Some (oper dst (SOp op) args rel)))::nil
+  | Iload trap chunk addr args dst pc' => (pc', (Some (oper dst (SLoad chunk addr) args rel)))::nil
+  | Icall _ _ _ dst pc' => (pc', (Some (kill_reg dst (kill_mem rel))))::nil
+  | Ibuiltin ef _ res pc' => (pc', (Some (kill_builtin_res res (apply_external_call ef rel))))::nil
+  | Itailcall _ _ _ | Ireturn _ => nil
   end.
   End PER_NODE.
 
-Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : abst_insn_out :=
-  match ro with
-  | None => Abst_same RB.bot
-  | Some x =>
-    match code ! pc with
-    | None => Abst_same RB.bot
-    | Some instr => apply_instr pc tenv instr x
+Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) :
+  list (node * RB.t)  :=
+  match code ! pc with
+  | None => nil
+  | Some instr => 
+    match ro with
+    | None => List.map (fun pc' => (pc', RB.bot)) (successors_instr instr)
+    | Some x => apply_instr pc tenv instr x
     end
   end.
 
@@ -507,12 +505,10 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva
          match PMap.get pc inv with
          | None => true
          | Some rel =>
-           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
+           List.forallb
+             (fun szz =>
+                relb_leb (snd szz) (PMap.get (fst szz) inv))
+             (apply_instr pc tenv instr rel)
          end).
 (* No longer used. Incompatible with transfer functions that yield a different result depending on the successor.