Merge pull request #193 from kth-step/riscv-symbexec

Symbolic exec checkpoint
kth-step · Nov 1, 2024 · 686f11d · 686f11d
2 parents 510af79 + ff853e4
commit 686f11d
Show file tree

Hide file tree

Showing 103 changed files with 9,677 additions and 3,219 deletions.
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -15,19 +15,20 @@ env:
 jobs:
   build:
     name: Build
-    runs-on: ubuntu-20.04
+    runs-on: ${{ matrix.os }}
 
     strategy:
       matrix:
-        polyml: [{version: 'v5.7.1'}, {version: 'v5.9.1', heapless: '1'}]
-        z3: ['4.8.4']
+        os: ['ubuntu-22.04']
+        polyml: [{version: 'PREPACKAGED'}, {version: 'v5.9.1', heapless: '1'}]
+        z3: ['4.13.0']
         hol4: ['trindemossen-1']
 
     env:
       HOLBA_POLYML_VERSION: ${{ matrix.polyml.version }}
       HOLBA_POLYML_HEAPLESS: ${{ matrix.polyml.heapless }}
       HOLBA_Z3_VERSION: ${{ matrix.z3 }}
-      HOLBA_Z3_ASSET_SUFFIX: '.d6df51951f4c-x64-debian-8.11.zip'
+      HOLBA_Z3_ASSET_SUFFIX: '-x64-glibc-2.35.zip'
       HOLBA_HOL4_VERSION: ${{ matrix.hol4 }}
 
     steps:
@@ -40,7 +41,7 @@ jobs:
         with:
           path: |
             ${{ env.HOLBA_OPT_DIR }}
-          key: os-${{ runner.os }}_polyml-${{ matrix.polyml }}_z3-${{ matrix.z3 }}_hol4-${{ matrix.hol4 }}
+          key: os-${{ matrix.os }}_polyml-${{ matrix.polyml.version }}_z3-${{ matrix.z3 }}_hol4-${{ matrix.hol4 }}
 
       - name: Static analysis
         timeout-minutes: 5
@@ -60,7 +61,7 @@ jobs:
           ./scripts/ci/run_holmake.sh
 
       - name: Run tests
-        timeout-minutes: 40
+        timeout-minutes: 55
         run: |
           ./scripts/ci/run_make.sh tests
 

diff --git a/examples/riscv/Holmakefile b/examples/riscv/Holmakefile
@@ -4,8 +4,7 @@ INCLUDES = $(HOLBADIR)/examples/riscv/swap \
            $(HOLBADIR)/examples/riscv/incr \
            $(HOLBADIR)/examples/riscv/incr-mem \
            $(HOLBADIR)/examples/riscv/mod2-mem \
-           $(HOLBADIR)/examples/riscv/isqrt \
-           $(HOLBADIR)/examples/riscv/aes
+           $(HOLBADIR)/examples/riscv/isqrt
 
 all: $(DEFAULT_TARGETS) test-riscv.exe
 .PHONY: all

diff --git a/examples/riscv/aes-unopt/aes_symb_execScript.sml b/examples/riscv/aes-unopt/aes_symb_execScript.sml
@@ -19,7 +19,10 @@ val _ = birs_auxLib.prepare_program_lookups bir_lift_thm;
 (* Symbolic analysis execution *)
 (* --------------------------- *)
 
-val (bsysprecond_thm, symb_analysis_thm) =
+(* turn on the store-store cheater *)
+val _ = birs_strategiesLib.birs_simp_select := birs_simp_instancesLib.birs_simp_default_riscv_gen true;
+
+val symb_analysis_thm =
  bir_symb_analysis_thm
   bir_aes_prog_def
   aes_init_addr_def [aes_end_addr_def]

diff --git a/examples/riscv/aes/Holmakefile b/examples/riscv/aes/Holmakefile
@@ -22,6 +22,14 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
 all: $(DEFAULT_TARGETS)
 .PHONY: all
 
+test-aes.exe: test-aes.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: test-aes.exe
+	./test-aes.exe
+
+EXTRA_CLEANS = test-aes.exe
+
 ifdef POLY
 ifndef HOLBA_POLYML_HEAPLESS
 HOLHEAP = $(HOLBADIR)/src/holba-heap

diff --git a/examples/riscv/aes/aes_symb_execScript.sml b/examples/riscv/aes/aes_symb_execScript.sml
@@ -17,7 +17,7 @@ val _ = birs_auxLib.prepare_program_lookups bir_lift_thm;
 (* Symbolic analysis execution *)
 (* --------------------------- *)
 
-val (bsysprecond_thm, symb_analysis_thm) =
+val symb_analysis_thm =
  bir_symb_analysis_thm
   bir_aes_prog_def
   aes_init_addr_def [aes_end_addr_def]
@@ -27,10 +27,6 @@ val (bsysprecond_thm, symb_analysis_thm) =
 
 val _ = show_tags := true;
 
-val _ = Portable.pprint Tag.pp_tag (tag bsysprecond_thm);
-
-Theorem aes_bsysprecond_thm = bsysprecond_thm
-
 val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
 
 Theorem aes_symb_analysis_thm = symb_analysis_thm

diff --git a/examples/riscv/aes/test-aes.sml b/examples/riscv/aes/test-aes.sml
@@ -0,0 +1,29 @@
+open HolKernel Parse boolLib bossLib;
+
+val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
+val _ = Globals.show_tags := true;
+
+open wordsTheory;
+
+open bir_programSyntax bir_program_labelsTheory bir_immTheory;
+
+open aes_symb_execTheory;
+
+(* for now we just have a leightweight check; this is to include aes into the test *)
+val _ = print "checking aes_symb_analysis_thm:\n";
+
+val term_sz = term_size (concl aes_symb_analysis_thm);
+val _ = print ("\nterm size = " ^ (Int.toString term_sz) ^ "\n\n");
+val expected_term_sz = 25198;
+
+val _ = if term_sz = expected_term_sz then () else
+        raise Fail "term size of aes symbolic execution theorem is not as expected";
+
+val triple_tm = ((snd o dest_comb o concl) aes_symb_analysis_thm);
+val [init_st_tm, prog_frag_L_tm, final_sts_tm] = pairSyntax.strip_pair triple_tm;
+val final_sts_birs_tm = final_sts_tm;
+
+val _ = if (length o pred_setSyntax.strip_set) final_sts_birs_tm = 1 then () else
+        raise Fail "number of final states is not as expected";
+
+val _ = print "ok!\n";