Fixes for new Holmake build

kth-step · Mar 4, 2024 · 0156594 · 0156594
1 parent f929ca5
commit 0156594
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 29 deletions.
diff --git a/Holmakefile b/Holmakefile
@@ -23,7 +23,8 @@ INCLUDES = $(HOLBADIR)/src/aux \
            $(HOLBADIR)/src/tools/scamv/obsmodel \
            $(HOLBADIR)/src/tools/scamv/persistence \
            $(HOLBADIR)/src/tools/scamv/symbexec \
-           $(HOLBADIR)/src/tools/scamv/proggen
+           $(HOLBADIR)/src/tools/scamv/proggen \
+           $(HOLBADIR)/src/tools/symbexec
 
 all: $(DEFAULT_TARGETS)
 .PHONY: all
diff --git a/src/tools/exec/examples/Holmakefile b/src/tools/exec/examples/Holmakefile
@@ -1,4 +0,0 @@
-INCLUDES = 
-
-all: $(DEFAULT_TARGETS)
-.PHONY: all

diff --git a/src/tools/symbexec/Holmakefile b/src/tools/symbexec/Holmakefile
@@ -0,0 +1,7 @@
+INCLUDES = $(HOLBADIR)/src/aux \
+           $(HOLBADIR)/src/theory/bir \
+           $(HOLBADIR)/src/theory/bir-support \
+           $(HOLBADIR)/src/theory/program_logic
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/src/tools/symbexec/Holmakefile.gen b/src/tools/symbexec/Holmakefile.gen
diff --git a/src/tools/symbexec/birs_rulesScript.sml b/src/tools/symbexec/birs_rulesScript.sml
@@ -139,19 +139,19 @@ val assert_spec_thm = store_thm(
     PAT_X_ASSUM ``!x. A`` (ASSUME_TAC o SPEC ``birs_symb_to_symbst <|bsst_pc := lbl2; bsst_environ := env2;
                   bsst_status := BST_AssertionViolated;
                   bsst_pcond :=
-                    BExp_BinExp BIExp_And pre (BExp_UnaryExp BIExp_Not cond')|>``) >>
+                    BExp_BinExp BIExp_And pre (BExp_UnaryExp BIExp_Not cond)|>``) >>
 
     FULL_SIMP_TAC (std_ss++birs_state_ss) [IMAGE_INSERT, IMAGE_EMPTY, birs_symb_to_symbst_def] >>
 
     `symb_pcondinf (bir_symb_rec_sbir bprog)
-          (BExp_BinExp BIExp_And pre (BExp_UnaryExp BIExp_Not cond'))` by (
+          (BExp_BinExp BIExp_And pre (BExp_UnaryExp BIExp_Not cond))` by (
       METIS_TAC [birs_pcondinf_thm, symb_symbst_pcond_def]
     ) >>
 
     FULL_SIMP_TAC (std_ss++symb_TYPES_ss) [symb_symbst_pcond_def, DIFF_INSERT, DIFF_EMPTY, DELETE_INSERT, EMPTY_DELETE] >>
     REV_FULL_SIMP_TAC (std_ss) [] >>
 
-    Q.ABBREV_TAC `sys2 = SymbSymbSt lbl1 env1 (BExp_BinExp BIExp_And pre cond') status` >>
+    Q.ABBREV_TAC `sys2 = SymbSymbSt lbl1 env1 (BExp_BinExp BIExp_And pre cond) status` >>
     Q.ABBREV_TAC `sys2' = SymbSymbSt lbl1 env1 pre status` >>
 
     ASSUME_TAC (

diff --git a/src/tools/symbexec/symb_record_soundScript.sml b/src/tools/symbexec/symb_record_soundScript.sml
@@ -583,12 +583,12 @@ val symb_subst_store_sound_NOTIN_thm = store_thm(
   REWRITE_TAC [boolTheory.FUN_EQ_THM] >>
   REPEAT STRIP_TAC >>
 
-  Cases_on `store' x` >- (
+  Cases_on `store x` >- (
     FULL_SIMP_TAC std_ss [symb_subst_store_thm]
   ) >>
 
   `symb NOTIN sr.sr_symbols_f x'` by (
-    `sr.sr_symbols_f x' SUBSET symb_symbols_store sr store'` by (
+    `sr.sr_symbols_f x' SUBSET symb_symbols_store sr store` by (
       METIS_TAC [symb_symbols_SUBSET_store_exps_thm]
     ) >>
     IMP_RES_TAC SUBSET_THM >>
@@ -645,7 +645,7 @@ val symb_subst_store_sound_thm = store_thm(
 
   EQ_TAC >> (
     REPEAT STRIP_TAC >>
-    Cases_on `store' var` >- (
+    Cases_on `store var` >- (
       METIS_TAC [symb_subst_store_thm, optionTheory.option_CLAUSES]
     ) >>
 
@@ -768,7 +768,7 @@ val symb_subst_store_symbols_thm3 = store_thm(
 
   Cases_on `?s. symb IN s ∧
               ?symbexp.
-                s = sr.sr_symbols_f symbexp /\ ?var. store' var = SOME symbexp` >- (
+                s = sr.sr_symbols_f symbexp /\ ?var. store var = SOME symbexp` >- (
     FULL_SIMP_TAC std_ss [] >>
     `sr.sr_symbols_f (sr.sr_subst_f (symb,symb_inst) symbexp) =
        (sr.sr_symbols_f symbexp DIFF {symb}) UNION (if symb IN sr.sr_symbols_f symbexp then sr.sr_symbols_f symb_inst else EMPTY)` by (