A little bit of poking at lemmas. Patch makefile to only use necessary

files for executable.
vellvm · Mar 27, 2024 · 74765d3 · 74765d3
1 parent c536e51
commit 74765d3
Show file tree

Hide file tree

Showing 2 changed files with 59 additions and 4 deletions.
diff --git a/src/Makefile b/src/Makefile
@@ -35,7 +35,10 @@ VELLVM_BC =_build/default/ml/main.bc
 FRONTEND_EXE=_build/default/ml/frontend.exe
 AGGREGATE_EXE=_build/default/ml/aggregate.exe
 COQFILES_FRONTEND := QC/ShowAST QC/ReprAST Utils/ParserHelper Syntax/LLVMAst Syntax/AstLib
+COQFILES_EXEC := QC/ShowAST QC/ReprAST Utils/ParserHelper Syntax/LLVMAst Syntax/AstLib Semantics/TopLevel Transformations/Transform Handlers/Handlers Theory/Refinement Utilities
 FRONTEND_VOFILES := $(COQFILES_FRONTEND:%=coq/%.vo)
+EXEC_VFILES := $(COQFILES_FRONTEND:%=coq/%.v)
+EXEC_VOFILES := $(COQFILES_EXEC:%=coq/%.vo)
 
 .DEFAULT_GOAL := all
 
@@ -70,7 +73,7 @@ coq: real-all
 .PHONY: extracted
 extracted: $(EXTRACTDIR)/STAMP
 
-$(EXTRACTDIR)/STAMP: $(VFILES) $(VOFILES) $(EXTRACTDIR)/Extract.v
+$(EXTRACTDIR)/STAMP: $(EXEC_VOFILES) $(EXTRACTDIR)/Extract.v
 	@echo "Extracting"
 	$(COQEXEC) $(EXTRACTDIR)/Extract.v
 	@echo "Patching extraction"

diff --git a/src/coq/Theory/OOMRefinementExamples.v b/src/coq/Theory/OOMRefinementExamples.v
@@ -428,8 +428,9 @@ Module Infinite.
           Vis (subevent _ (Alloca (DTYPE_I 64) 1 None))
           (fun u => Vis (subevent _ (LocalWrite (Name "ptr") (dvalue_to_uvalue u)))
                       (fun x => Vis (subevent _ (LocalRead (Name "ptr")))
-                                (fun u1 => Vis (subevent _ (LocalWrite (Name "i") (UVALUE_Conversion Ptrtoint DTYPE_Pointer u1 DTYPE_IPTR)))
-                                            (fun _ => Ret (DVALUE_I1 Int1.one))))).
+                               (fun u1 => u <- concretize_if_no_undef_or_poison (UVALUE_Conversion Ptrtoint DTYPE_Pointer u1 DTYPE_IPTR);;
+                                       Vis (subevent _ (LocalWrite (Name "i") u))
+                                         (fun _ => Ret (DVALUE_I1 Int1.one))))).
   Proof.
     unfold interp_instr_E_to_L0.
     unfold ptoi_tree. cbn. go. cbn. go.
@@ -451,7 +452,58 @@ Module Infinite.
     eapply eqit_Vis.
     intros. force_go.
     rewrite bind_tau. go. rewrite tau_eutt.
-    force_go. cbn. rewrite bind_trigger.
+    force_go. cbn.
+    rewrite interp_translate.
+    eapply eqit_bind'.
+    { (* TODO: Make this a lemma *)
+      cbn.
+      unfold concretize_if_no_undef_or_poison.
+      cbn.
+      break_match.
+      - force_go. reflexivity.
+      - force_go. cbn.
+        setoid_rewrite concretize_uvalue_err_ub_oom_to_itree.
+        remember (concretize_uvalue u1) as conc.
+        Import Monad ITreeMonad.
+        destruct_err_ub_oom conc.
+        + setoid_rewrite raiseOOM_bind_itree.
+          setoid_rewrite interp_trigger.
+          rewrite interp_translate.
+          unfold raiseOOM.
+          setoid_rewrite bind_trigger.
+          force_go; cbn.
+          setoid_rewrite bind_trigger; cbn.
+          eapply eqit_Vis.
+          intros [].
+        + setoid_rewrite raiseUB_bind_itree.
+          rewrite interp_translate.
+          unfold raiseUB.
+          setoid_rewrite bind_trigger.
+          force_go; cbn.
+          setoid_rewrite bind_trigger; cbn.
+          eapply eqit_Vis.
+          intros [].
+        + setoid_rewrite raise_bind_itree.
+          rewrite interp_translate.
+          unfold raise.
+          setoid_rewrite bind_trigger.
+          force_go; cbn.
+          setoid_rewrite bind_trigger; cbn.
+          eapply eqit_Vis.
+          intros [].
+        + cbn. go.
+          rewrite translate_bind.
+          rewrite interp_bind.
+          setoid_rewrite translate_ret.
+          setoid_rewrite interp_ret.
+          rewrite interp_translate.
+          cbn.
+          eapply eqit_bind'.
+          { rewrite interp_trigger_h.
+          }
+    }
+    eapply eqit_clos_bind.
+    rewrite bind_trigger.
 
     eapply eqit_Vis.
     intros. force_go.