Merge pull request kth-step#186 from kth-step/aux-to-extra

aux to extra, separation between bir and non-bir libraries/theories

Holmakefile

@@ -1,6 +1,6 @@
 CLINE_OPTIONS = -r
 
-INCLUDES = $(HOLBADIR)/src/aux \
+INCLUDES = $(HOLBADIR)/src/extra \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/shared/HolSmt \
            $(HOLBADIR)/src/shared/sml-simplejson \

README.md

@@ -72,37 +72,40 @@ cd examples
 ${HOLBA_HOLMAKE}
 ```
 
-## Directories and organization
-
-```
-├─ doc: Documentation material
-├─ examples: Showcasing HolBA
-│  ├─ aes: lifting + WP of AES on ARMv8 and for Cortex-M0
-│  ├─ bsl-wp-smt: Small BIR example programs to test simplified BIR generation, WP propagation and SMT interface
-│  ├─ nic: NIC formalization
-│  ├─ tutorial: End-to-end tutorial of simple ARMv8 examples
-├─ scripts: CI and installation scripts
-└─ src
-   ├─ aux: Non-HolBA-specific theories and libraries
-   ├─ shared: Libraries shared between tools
-   ├─ theory
-   │  ├─ abstract-hoare-logic: Abstract Hoare-style logic for unstructured code
-   │  ├─ bir: Core BIR language
-   │  ├─ bir-support: Extensions and supporting theories for BIR
-   │  ├─ models: Additional machine models
-   │  └─ tools: Theories for the tool libraries in src/tools
-   └─ tools
-      ├─ backlifter: Gets ISA-level contracts from BIR contracts
-      ├─ cfg: Control Flow Graph utilities
-      ├─ comp: Composition of contracts
-      ├─ exec: Concrete execution
-      ├─ lifter: Transpiler from binary to BIR
-      ├─ pass: Passification utility
-      ├─ scamv: Abstract side channel model validation framework
-      └─ wp: Weakest precondition propagation
-```
-
-### Tools status
+## Library organization
+
+### Directory structure
+
+- `doc`: Documentation about HolBA and BIR
+- `examples`: Applications of HolBA
+  - `aes`: lifting + WP of an AES block cipher implementation on ARMv8 and Cortex-M0
+  - `bsl-wp-smt`: Small BIR example programs to test simplified BIR generation, WP propagation and SMT interface
+  - `ijr`: Theory and examples related to indirect jumps
+  - `nic`: Network interface controller formalization
+  - `riscv`: Examples of specifying and verifying RISC-V programs
+  - `tutorial`: End-to-end tutorial of simple ARMv8 example programs
+- `scripts`: CI and installation scripts
+- `src`: Library sources
+  - `extra`: General theories and libraries
+  - `shared`: Libraries shared between tools
+  - `theory`: Domain-specific theories
+    - `bir`: Core BIR language
+    - `bir-support`: Extensions and supporting theories for BIR
+    - `models`: Additional machine models
+    - `program_logic`: Abstract Hoare-style logic for unstructured code
+    - `tools`: Theories for the tool libraries in `src/tools`
+  - `tools`: Domain-specific libraries
+    - `backlifter`: Utilities for obtaining ISA-level contracts from BIR contracts
+    - `cfg`: Control flow graph utilities
+    - `comp`: Composition of contracts
+    - `compute`: Utilities for using `cv_compute` in HOL4
+    - `exec`: Concrete execution
+    - `lifter`: Translation from binary ISA code to BIR
+    - `pass`: Passification utility
+    - `scamv`: Abstract side channel model validation framework
+    - `wp`: Weakest precondition propagation
+
+### Tool status
 
 - `tools/backlifter`:
   * Proof-producing

examples/aes/wp/aesWpExport.sml

@@ -7,7 +7,7 @@ open bir_typing_progTheory;
 open bir_envTheory;
 open bir_exp_substitutionsTheory;
 open bir_bool_expTheory;
-open bir_auxiliaryTheory;
+open holba_auxiliaryTheory;
 open bir_valuesTheory;
 open bir_expTheory;
 open bir_program_env_orderTheory;

examples/ijr/contractTransferScript.sml

@@ -4,10 +4,10 @@ open listTheory pred_setTheory pred_setSimps;
 
 open bir_programTheory bir_htTheory bir_program_multistep_propsTheory;
 open HolBACoreSimps;
-open bir_wm_instTheory bir_auxiliaryTheory;
+open bir_wm_instTheory holba_auxiliaryTheory;
 open abstract_simp_hoare_logicTheory abstract_hoare_logicTheory;
 open abstract_hoare_logicSimps bir_program_env_orderTheory bir_env_oldTheory;
-open bir_auxiliaryLib;
+open holba_auxiliaryLib;
 
 open resolutionTheory simulationTheory simulationFailTheory;
 

examples/ijr/resolveFullyScript.sml

@@ -61,7 +61,7 @@ CASE_TAC >- (
 FULL_SIMP_TAC (list_ss++bir_TYPES_ss) [fresh_label_def, direct_jump_target_def,
                                        bir_get_current_block_def, bir_block_pc_def,
                                        bir_get_program_block_info_by_label_def] >>
-SIMP_TAC std_ss [Once bir_auxiliaryTheory.INDEX_FIND_INDEX_CHANGE] >>
+SIMP_TAC std_ss [Once holba_auxiliaryTheory.INDEX_FIND_INDEX_CHANGE] >>
 Q.PAT_X_ASSUM ‘∀l'' bl. _’ (MP_TAC o Q.SPECL [‘l'’, ‘bl’]) >>
 EVERY_CASE_TAC >>
 FULL_SIMP_TAC std_ss [] >>

examples/ijr/resolveScript.sml

@@ -38,7 +38,7 @@ REPEAT GEN_TAC >- (
 SIMP_TAC list_ss [] >>
 ASM_SIMP_TAC arith_ss [INDEX_FIND_def] >>
 REPEAT STRIP_TAC >>
-MP_TAC (Q.SPECL [‘SUC n’, ‘n'’, ‘P’, ‘(xs ++ ys)’, ‘x’] bir_auxiliaryTheory.INDEX_FIND_PRE) >>
+MP_TAC (Q.SPECL [‘SUC n’, ‘n'’, ‘P’, ‘(xs ++ ys)’, ‘x’] holba_auxiliaryTheory.INDEX_FIND_PRE) >>
 ASM_SIMP_TAC std_ss []
 QED
 

examples/ijr/simulationFailScript.sml

@@ -3,7 +3,7 @@ open HolKernel Parse boolLib bossLib;
 open listTheory pred_setSimps;
 
 open bir_programTheory bir_expTheory bir_exp_immTheory bir_typing_expTheory;
-open bir_valuesTheory bir_auxiliaryTheory
+open bir_valuesTheory holba_auxiliaryTheory
 open bir_program_blocksTheory bir_program_multistep_propsTheory;
 open HolBACoreSimps;
 

examples/riscv/common/bir_symbLib.sml

@@ -24,15 +24,15 @@ fun bir_symb_analysis bprog_tm birs_state_init_lbl
      bsst_status   := BST_Running;
      bsst_pcond    := ^birs_pcond
    |>``;
-   val timer_symbanalysis = bir_miscLib.timer_start 0;
-   val timer_symbanalysis_last = ref (bir_miscLib.timer_start 0);
+   val timer_symbanalysis = holba_miscLib.timer_start 0;
+   val timer_symbanalysis_last = ref (holba_miscLib.timer_start 0);
    val birs_rule_STEP_thm = birs_rule_STEP_prog_fun (bir_prog_has_no_halt_fun bprog_tm);
    val birs_rule_SUBST_thm = birs_rule_SUBST_prog_fun bprog_tm;
    val birs_post_step_fun =
      (fn t => (
-        bir_miscLib.timer_stop (fn delta_s => print ("running since " ^ delta_s ^ "\n")) timer_symbanalysis;
-        bir_miscLib.timer_stop (fn delta_s => print ("time since last step " ^ delta_s ^ "\n")) (!timer_symbanalysis_last);
-        timer_symbanalysis_last := bir_miscLib.timer_start 0;
+        holba_miscLib.timer_stop (fn delta_s => print ("running since " ^ delta_s ^ "\n")) timer_symbanalysis;
+        holba_miscLib.timer_stop (fn delta_s => print ("time since last step " ^ delta_s ^ "\n")) (!timer_symbanalysis_last);
+        timer_symbanalysis_last := holba_miscLib.timer_start 0;
 	(*print_term ((last o pairSyntax.strip_pair o snd o dest_comb o concl) t);*)
 	t)) o
      birs_rule_SUBST_trysimp_fun birs_rule_SUBST_thm o
@@ -56,12 +56,12 @@ fun bir_symb_analysis bprog_tm birs_state_init_lbl
      birs_rule_STEP_SEQ_fun (birs_rule_SUBST_thm, birs_rule_STEP_SEQ_thm));
 
    val _ = print "now reducing it to one sound structure\n";
-   val timer = bir_miscLib.timer_start 0;
+   val timer = holba_miscLib.timer_start 0;
    val result = exec_until
      (birs_rule_STEP_fun_spec, birs_rule_SEQ_fun_spec, birs_rule_STEP_SEQ_fun_spec)
      single_step_A_thm birs_end_lbls
      handle e => (Profile.print_profile_results (Profile.results ()); raise e);
-   val _ = bir_miscLib.timer_stop
+   val _ = holba_miscLib.timer_stop
     (fn delta_s => print ("\n======\n > exec_until took " ^ delta_s ^ "\n")) timer;
 
 (*
@@ -81,7 +81,7 @@ fun bir_symb_analysis_thm bir_prog_def
  init_addr_def end_addr_defs bspec_pre_def birenvtyl_def =
  let
    val _ = print "\n======\n > bir_symb_analysis_thm started\n";
-   val timer = bir_miscLib.timer_start 0;
+   val timer = holba_miscLib.timer_start 0;
    val bprog_tm = (fst o dest_eq o concl) bir_prog_def;
    val init_addr_tm = (snd o dest_eq o concl) init_addr_def;
    val birs_state_init_lbl_tm =
@@ -106,7 +106,7 @@ fun bir_symb_analysis_thm bir_prog_def
    val symb_analysis_thm = bir_symb_analysis
     bprog_tm birs_state_init_lbl_tm birs_state_end_tm_lbls
     birs_env_tm birs_pcond_tm;
-   val _ = bir_miscLib.timer_stop (fn delta_s => print ("\n======\n > bir_symb_analysis_thm took " ^ delta_s ^ "\n")) timer;
+   val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > bir_symb_analysis_thm took " ^ delta_s ^ "\n")) timer;
    val symb_analysis_fix_thm = REWRITE_RULE [GSYM birs_env_thm] symb_analysis_thm;
  in
    (bsysprecond_thm, symb_analysis_fix_thm)

examples/riscv/perftest/simpstress.sml

@@ -7078,12 +7078,12 @@ val bprog_tm = (fst o dest_eq o concl) bir_aespart_prog_def;
    val birs_rule_STEP_thm = birs_rule_STEP_prog_fun (bir_prog_has_no_halt_fun bprog_tm);
    val birs_rule_SUBST_thm = birs_rule_SUBST_prog_fun bprog_tm;
 
-   val timer_symbanalysis_last = ref (bir_miscLib.timer_start 0);
+   val timer_symbanalysis_last = ref (holba_miscLib.timer_start 0);
 
    val birs_post_step_fun =
      (fn t => (
-        bir_miscLib.timer_stop (fn delta_s => print ("time since last step " ^ delta_s ^ "\n")) (!timer_symbanalysis_last);
-        timer_symbanalysis_last := bir_miscLib.timer_start 0;
+        holba_miscLib.timer_stop (fn delta_s => print ("time since last step " ^ delta_s ^ "\n")) (!timer_symbanalysis_last);
+        timer_symbanalysis_last := holba_miscLib.timer_start 0;
 	(*print_term ((last o pairSyntax.strip_pair o snd o dest_comb o concl) t);*)
 	t)) o
      birs_rule_SUBST_trysimp_fun birs_rule_SUBST_thm o
@@ -7097,7 +7097,7 @@ val bprog_tm = (fst o dest_eq o concl) bir_aespart_prog_def;
 
 (* ================================================================================= *)
 (*
-   val timer_symbanalysis_last = ref (bir_miscLib.timer_start 0);
+   val timer_symbanalysis_last = ref (holba_miscLib.timer_start 0);
 val _ = birs_rule_STEP_fun_spec state2;
 *)
 
@@ -7120,7 +7120,7 @@ val _ = print "\n";
 val _ = Profile.print_profile_results (Profile.results ());
 
 (*
-val teststring = bir_fileLib.read_from_file "/home/andreas/data/hol/HolBA_symbexec/examples/riscv/perftest/tempdir/smtquery_2024-08-08_11-38-51_253062_nil";
+val teststring = holba_fileLib.read_from_file "/home/andreas/data/hol/HolBA_symbexec/examples/riscv/perftest/tempdir/smtquery_2024-08-08_11-38-51_253062_nil";
 
 
 val z3bin = "/home/andreas/data/hol/HolBA_opt/z3-4.8.4/bin/z3";

examples/tutorial/7-composition/mutrec_compositionScript.sml

@@ -10,7 +10,7 @@ open bir_prog_mutrecTheory;
 open mutrec_wpTheory;
 open mutrec_smtTheory;
 
-open bir_auxiliaryLib;
+open holba_auxiliaryLib;
 
 open HolBACoreSimps;
 open HolBASimps;

examples/tutorial/support2/bir_symb2_execScript.sml

@@ -2,15 +2,15 @@
 (*
 app load ["HolKernel", "Parse", "boolLib" ,"bossLib"];
 app load ["wordsTheory", "bitstringTheory"];
-app load ["bir_auxiliaryTheory", "bir_immTheory", "bir_valuesTheory"];
+app load ["holba_auxiliaryTheory", "bir_immTheory", "bir_valuesTheory"];
 app load ["bir_symb2_envTheory"];
 app load ["bir_programTheory", "bir_expTheory", "bir_envTheory"];
 app load ["llistTheory", "wordsLib"];
 *)
 
 open HolKernel Parse boolLib bossLib;
 open wordsTheory bitstringTheory;
-open bir_auxiliaryTheory bir_immTheory bir_valuesTheory;
+open holba_auxiliaryTheory bir_immTheory bir_valuesTheory;
 open bir_envTheory;
 open bir_expTheory;
 open bir_programTheory;

src/aux/bir_auxiliaryLib.sig → src/extra/holba_auxiliaryLib.sig

@@ -1,4 +1,4 @@
-signature bir_auxiliaryLib =
+signature holba_auxiliaryLib =
 sig
   include Abbrev
   type simpset = simpLib.simpset

src/aux/bir_auxiliaryLib.sml → src/extra/holba_auxiliaryLib.sml

@@ -1,4 +1,4 @@
-structure bir_auxiliaryLib :> bir_auxiliaryLib =
+structure holba_auxiliaryLib :> holba_auxiliaryLib =
 struct
 
 open HolKernel boolLib liteLib simpLib Parse bossLib;

src/aux/bir_auxiliaryScript.sml → src/extra/holba_auxiliaryScript.sml

@@ -1,11 +1,11 @@
 open HolKernel Parse boolLib bossLib;
 
-open bir_auxiliaryLib;
+open holba_auxiliaryLib;
 
 open wordsTheory bitstringTheory ASCIInumbersTheory;
 open pred_setTheory;
 
-val _ = new_theory "bir_auxiliary";
+val _ = new_theory "holba_auxiliary";
 
 (* -------------------------------------------------------------------------- *)
 (* List lemmata                                                               *)

src/extra/holba_eq_utilLib.sig

@@ -0,0 +1,8 @@
+signature holba_eq_utilLib =
+sig
+  val assoc_with : ('b * 'b -> bool) -> 'b -> ('b * 'a) list -> 'a;
+
+  val rev_assoc_with : ('a * 'a -> bool) -> 'a -> ('b * 'a) list -> 'b;
+
+  val mem_with : ('a * 'a -> bool) -> 'a -> 'a list -> bool;
+end

src/aux/bir_eq_utilLib.sml → src/extra/holba_eq_utilLib.sml

@@ -1,10 +1,10 @@
-structure bir_eq_utilLib =
+structure holba_eq_utilLib :> holba_eq_utilLib =
 struct
 
 local
   open HolKernel Parse;
 
-  val ERR = mk_HOL_ERR "bir_eq_utilLib"
+  val ERR = mk_HOL_ERR "holba_eq_utilLib"
 in
 
 (* val assoc_with : ('b * 'b -> bool) -> 'b -> ('b * 'a) list -> 'a *)

src/shared/bir_smtLib.sml

@@ -3,8 +3,8 @@ struct
 
 local
 
-  open bir_fileLib;
-  open bir_exec_wrapLib;
+  open holba_fileLib;
+  open holba_exec_wrapLib;
 
   val ERR = Feedback.mk_HOL_ERR "bir_smtLib";
 
@@ -189,7 +189,7 @@ local
   open bir_valuesSyntax;
   open wordsSyntax;
 
-  open bir_fileLib;
+  open holba_fileLib;
 
   val ERR = Feedback.mk_HOL_ERR "bir_smtLib";
 

src/shared/examples/test-json.sml

@@ -9,7 +9,7 @@ val _ = load "sml-simplejson/jsonparse";
 *)
 
 fun readFile filename =
-  String.concat (bir_fileLib.read_file_lines filename);
+  String.concat (holba_fileLib.read_file_lines filename);
 
 fun parseJson input =
     let
@@ -264,7 +264,7 @@ val jsonarg = Json.STRING (term_to_string t);
 
 val command = "./try_deserialize_serialize_json.py";
 val operation = "test";
-val jsonback = bir_json_execLib.call_json_exec (command, ["-v", operation], jsonarg);
+val jsonback = holba_json_execLib.call_json_exec (command, ["-v", operation], jsonarg);
 
 val stringback = case jsonback of
                     Json.STRING s => s
@@ -280,7 +280,7 @@ end
 val command = "./try_deserialize_serialize_json.py";
 val operation = "wrong";
 val jsonarg = Json.STRING "";
-val r = (bir_json_execLib.call_json_exec (command, ["-v", operation], jsonarg); true)
+val r = (holba_json_execLib.call_json_exec (command, ["-v", operation], jsonarg); true)
         handle _ => false;
 
 val _ = if not r then () else

src/shared/examples/test-z3_wrapper.sml

@@ -85,14 +85,14 @@ val _ = List.map (fn (name, query, expected) =>
 
 
 (* test of real input, comparison. it is quite rigid in terms of output requirement *)
-open bir_fileLib;
+open holba_fileLib;
 
 val filename = "z3_wrapper_test/z3_wrapper_input_z3_T5bnC5_sat";
 val _ = print ("\n\n=============== >>> RUNNING TEST CASE FILE '" ^ filename ^ "'\n");
 
 val expected_output = read_from_file (filename ^ "_expectedoutput");
 
-val output = bir_exec_wrapLib.get_exec_output ("../z3_wrapper.py " ^ filename);
+val output = holba_exec_wrapLib.get_exec_output ("../z3_wrapper.py " ^ filename);
 
 val _ = if output = expected_output then () else (
             print "=============== >>> TEST CASE FAILED\n";

src/shared/bir_exec_wrapLib.sml → src/shared/holba_exec_wrapLib.sml

@@ -1,10 +1,10 @@
-structure bir_exec_wrapLib =
+structure holba_exec_wrapLib =
 struct
 local
-  val ERR = Feedback.mk_HOL_ERR "bir_exec_wrapLib"
-  val wrap_exn = Feedback.wrap_exn "bir_exec_wrapLib"
+  val ERR = Feedback.mk_HOL_ERR "holba_exec_wrapLib"
+  val wrap_exn = Feedback.wrap_exn "holba_exec_wrapLib"
 
-  open bir_fileLib;
+  open holba_fileLib;
 
 in
 

src/shared/bir_fileLib.sml → src/shared/holba_fileLib.sml

@@ -1,10 +1,10 @@
-structure bir_fileLib =
+structure holba_fileLib =
 struct
 local
-  val ERR = Feedback.mk_HOL_ERR "bir_fileLib"
-  val wrap_exn = Feedback.wrap_exn "bir_fileLib"
+  val ERR = Feedback.mk_HOL_ERR "holba_fileLib"
+  val wrap_exn = Feedback.wrap_exn "holba_fileLib"
 
-  open bir_miscLib;
+  open holba_miscLib;
 
 in