CSE3 analysis

3 files changed, 81 insertions, 6 deletions

diff --git a/backend/CSE3.v b/backend/CSE3.v
index d54b9ffa..f8a25515 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -69,7 +69,7 @@ Definition transf_function (f: function) : res function :=
   do tenv <- type_function f;
   let (invariants, hints) := preanalysis tenv f in
   let ctx := context_from_hints hints in
-  if check_inductiveness (ctx:=ctx) tenv invariants f
+  if check_inductiveness (ctx:=ctx) f tenv invariants
   then
     OK {| fn_sig := f.(fn_sig);
           fn_params := f.(fn_params);
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 43c44ccd..76723f40 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -331,16 +331,16 @@ Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t
 
 Definition invariants := PMap.t RB.t.
 
-Definition rel_le (x y : RELATION.t) : bool := (PSet.is_subset y x).
+Definition rel_leb (x y : RELATION.t) : bool := (PSet.is_subset y x).
 
-Definition relb_le (x y : RB.t) : bool :=
+Definition relb_leb (x y : RB.t) : bool :=
   match x, y with
   | None, _ => true
   | (Some _), None => false
-  | (Some x), (Some y) => rel_le x y
+  | (Some x), (Some y) => rel_leb x y
   end.
 
-Definition check_inductiveness (tenv: typing_env) (inv: invariants) (fn : RTL.function) :=
+Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: invariants) :=
   (RB.beq (Some RELATION.top) (PMap.get (fn_entrypoint fn) inv)) &&
   PTree_Properties.for_all (fn_code fn) 
       (fun pc instr =>
@@ -349,7 +349,7 @@ Definition check_inductiveness (tenv: typing_env) (inv: invariants) (fn : RTL.fu
          | Some rel =>
            let rel' := apply_instr pc tenv instr rel in
            List.forallb
-             (fun pc' => relb_le rel' (PMap.get pc' inv))
+             (fun pc' => relb_leb rel' (PMap.get pc' inv))
              (RTL.successors_instr instr)
          end).
 
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 05c7a8f3..5514c532 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -10,6 +10,26 @@ Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet.
 Require Import RTLtyping.
 Require Import Lia.
 
+Lemma rel_leb_correct:
+  forall x x',
+    rel_leb x x' = true <-> RELATION.ge x' x.
+Proof.
+  unfold rel_leb, RELATION.ge.
+  split; auto.
+Qed.
+
+Hint Resolve rel_leb_correct : cse3.
+
+Lemma relb_leb_correct:
+  forall x x',
+    relb_leb x x' = true <-> RB.ge x' x.
+Proof.
+  unfold relb_leb, RB.ge.
+  destruct x; destruct x'; split; trivial; try contradiction; discriminate.
+Qed.
+
+Hint Resolve relb_leb_correct : cse3.
+
 Theorem loadv_storev_really_same:
   forall chunk: memory_chunk,
   forall m1: mem,
@@ -708,4 +728,59 @@ Section SOUNDNESS.
     rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial.
     assumption.
   Qed.
+
+  Hint Resolve store_sound : cse3.
+
+  Section INDUCTIVENESS.
+    Variable fn : RTL.function.
+    Variable tenv : typing_env.
+    Variable inv: invariants.
+    
+    Definition is_inductive_step (pc pc' : node) :=
+      forall instr,
+        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)).
+
+    Definition is_inductive_allstep :=
+      forall pc pc', is_inductive_step pc pc'.
+
+    Lemma checked_is_inductive_allstep:
+      (check_inductiveness (ctx:=ctx) fn tenv inv) = true ->
+      is_inductive_allstep.
+    Proof.
+      unfold check_inductiveness, is_inductive_allstep, is_inductive_step.
+      rewrite andb_true_iff.
+      rewrite PTree_Properties.for_all_correct.
+      intros (ENTRYPOINT & ALL).
+      intros until instr.
+      intros INSTR IN_SUCC.
+      specialize ALL with (x := pc) (a := instr).
+      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.
+    Qed.
+    
+    Lemma checked_is_inductive_entry:
+      (check_inductiveness (ctx:=ctx) fn tenv inv) = true ->
+      inv # (fn_entrypoint fn) = Some RELATION.top.
+    Proof.
+      unfold check_inductiveness, is_inductive_allstep, is_inductive_step.
+      rewrite andb_true_iff.
+      intros (ENTRYPOINT & ALL).
+      apply RB.beq_correct in ENTRYPOINT.
+      unfold RB.eq, RELATION.eq in ENTRYPOINT.
+      destruct (inv # (fn_entrypoint fn)) as [rel | ].
+      2: contradiction.
+      f_equal.
+      symmetry.
+      assumption.
+    Qed.
+  End INDUCTIVENESS.
 End SOUNDNESS.