Add function to reason about executable constraints

1 files changed, 11 insertions, 1 deletions

diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 2c7bfc8..0462e28 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -238,7 +238,7 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest
                              (f #r (Reg r))
                              (seq_app (pred_ret (Eop op)) (merge (list_translation rl f))));
       Some (pred, f #r (Reg r) <- pruned)
-  | RBload p chunk addr rl r =>
+  | RBload  p chunk addr rl r =>
       do pruned <-
            prune_predicated
              (app_predicated (dfltp p ∧ pred)
@@ -277,6 +277,16 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest
       Some (new_p, f <-e pruned)
   end.
 
+Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr :=
+  match i with
+  | RBnop => lst
+  | RBop p op rl r => (f #r (Reg r)) :: lst
+  | RBload  p chunk addr rl r => (f #r (Reg r)) :: lst
+  | RBstore p chunk addr rl r => (f #r Mem) :: lst
+  | RBsetpred p' c args p => lst
+  | RBexit p c => lst
+  end.
+
 (*|
 Implementing which are necessary to show the correctness of the translation
 validation by showing that there aren't any more effects in the resultant RTLPar