Make z3 prelude autogenerated and based on a set of easily adjustable…

… parameters
kth-step · Aug 29, 2024 · 45bf1e6 · 45bf1e6
1 parent fd1a3a8
commit 45bf1e6
Show file tree

Hide file tree

Showing 4 changed files with 208 additions and 167 deletions.
diff --git a/src/shared/smt/bir_smtlibLib.z3_prelude b/src/shared/smt/bir_smtlibLib.z3_prelude
diff --git a/src/shared/smt/holba_z3Lib.sml b/src/shared/smt/holba_z3Lib.sml
@@ -24,8 +24,8 @@ fun get_streams p = Unix.streamsOf p;
 
 val z3proc_bin_o = ref (NONE : string option);
 val z3proc_o = ref (NONE : ((TextIO.instream, TextIO.outstream) Unix.proc) option);
-val bir_smtLib_z3_prelude = read_from_file (holpathdb.subst_pathvars "$(HOLBADIR)/src/shared/smt/bir_smtlibLib.z3_prelude");
-val bir_smtLib_z3_prelude_n = bir_smtLib_z3_prelude ^ "\n";
+val prelude_z3 = read_from_file (holpathdb.subst_pathvars "$(HOLBADIR)/src/shared/smt/holba_z3Lib_prelude.z3");
+val prelude_z3_n = prelude_z3 ^ "\n";
 val use_stack = true;
 val debug_print = false;
 fun get_z3proc z3bin =
@@ -49,7 +49,7 @@ fun get_z3proc z3bin =
 	 let
           val (_,s_out) = get_streams p;
           (* prepare prelude and push *)
-          val () = TextIO.output (s_out, bir_smtLib_z3_prelude ^ "\n");
+          val () = TextIO.output (s_out, prelude_z3 ^ "\n");
           val () = TextIO.output (s_out, "(push)\n");
 	 in
 	  ()
@@ -81,7 +81,7 @@ fun sendreceive_query z3bin q =
    val p = get_z3proc z3bin;
    val (s_in,s_out) = get_streams p;
    val _ = if not use_stack then
-            TextIO.output (s_out, bir_smtLib_z3_prelude_n)
+            TextIO.output (s_out, prelude_z3_n)
            else ();
 
    val timer = holba_miscLib.timer_start 0;
@@ -283,11 +283,14 @@ val valad = ("mem_ad1", SMTTY_BV szadi);
 val valv = ("mem_v1", SMTTY_BV szi);
 *)
 fun gen_smt_load_as_exp valm valad (endi, szadi, szci, szi) =
+  (* special case for szci = szi *)
+  if szci = szi then
+    gen_smtlib_expr "select" [valm, valad] (SMTTY_BV szi)
+  else
   let
           val revfun =
 	    if endi = SMTMEM_LittleEndian then List.rev else
 	    if endi = SMTMEM_BigEndian then I else
-	    if endi = SMTMEM_NoEndian andalso szci = szi then I else
             raise ERR "gen_smt_load_as_exp" "unsupported combination of endianness and memory dimension";
 
           fun gen_addr_const i = "(_ bv" ^ (Int.toString i) ^ " " ^ (Int.toString szadi) ^ ")";
@@ -300,11 +303,14 @@ fun gen_smt_load_as_exp valm valad (endi, szadi, szci, szi) =
   end;
 
 fun gen_smt_store_as_exp valm valad valv (endi, szadi, szci, szi) =
+  (* special case for szci = szi *)
+  if szci = szi then
+    gen_smtlib_expr "store" [valm, valad, valv] (snd valm)
+  else
   let
           val revfun =
 	    if endi = SMTMEM_LittleEndian then List.rev else
 	    if endi = SMTMEM_BigEndian then I else
-	    if endi = SMTMEM_NoEndian andalso szci = szi then I else
             raise ERR "gen_smt_load_as_exp" "unsupported combination of endianness and memory dimension";
 
           fun gen_addr_const i = "(_ bv" ^ (Int.toString i) ^ " " ^ (Int.toString szadi) ^ ")";

diff --git a/src/shared/smt/holba_z3Lib_prelude.z3 b/src/shared/smt/holba_z3Lib_prelude.z3
@@ -0,0 +1,89 @@
+; memory 32->8 (LE)
+; ----------------------
+(define-fun loadfun_LE_32_8_8
+  ((a (Array (_ BitVec 32) (_ BitVec 8))) (ad (_ BitVec 32)))
+  (_ BitVec 8)
+  (select a ad)
+)
+(define-fun loadfun_LE_32_8_16
+  ((a (Array (_ BitVec 32) (_ BitVec 8))) (ad (_ BitVec 32)))
+  (_ BitVec 16)
+  (concat (select a (bvadd ad (_ bv1 32))) (select a (bvadd ad (_ bv0 32))))
+)
+(define-fun loadfun_LE_32_8_32
+  ((a (Array (_ BitVec 32) (_ BitVec 8))) (ad (_ BitVec 32)))
+  (_ BitVec 32)
+  (concat (select a (bvadd ad (_ bv3 32))) (select a (bvadd ad (_ bv2 32))) (select a (bvadd ad (_ bv1 32))) (select a (bvadd ad (_ bv0 32))))
+)
+(define-fun loadfun_LE_32_8_64
+  ((a (Array (_ BitVec 32) (_ BitVec 8))) (ad (_ BitVec 32)))
+  (_ BitVec 64)
+  (concat (select a (bvadd ad (_ bv7 32))) (select a (bvadd ad (_ bv6 32))) (select a (bvadd ad (_ bv5 32))) (select a (bvadd ad (_ bv4 32))) (select a (bvadd ad (_ bv3 32))) (select a (bvadd ad (_ bv2 32))) (select a (bvadd ad (_ bv1 32))) (select a (bvadd ad (_ bv0 32))))
+)
+
+(define-fun storefun_LE_32_8_8
+  ((a (Array (_ BitVec 32) (_ BitVec 8))) (ad (_ BitVec 32)) (v (_ BitVec 8)))
+  (Array (_ BitVec 32) (_ BitVec 8))
+  (store a ad v)
+)
+(define-fun storefun_LE_32_8_16
+  ((a (Array (_ BitVec 32) (_ BitVec 8))) (ad (_ BitVec 32)) (v (_ BitVec 16)))
+  (Array (_ BitVec 32) (_ BitVec 8))
+  (store (store a (bvadd ad (_ bv1 32)) ((_ extract 15 8) v)) (bvadd ad (_ bv0 32)) ((_ extract 7 0) v))
+)
+(define-fun storefun_LE_32_8_32
+  ((a (Array (_ BitVec 32) (_ BitVec 8))) (ad (_ BitVec 32)) (v (_ BitVec 32)))
+  (Array (_ BitVec 32) (_ BitVec 8))
+  (store (store (store (store a (bvadd ad (_ bv3 32)) ((_ extract 31 24) v)) (bvadd ad (_ bv2 32)) ((_ extract 23 16) v)) (bvadd ad (_ bv1 32)) ((_ extract 15 8) v)) (bvadd ad (_ bv0 32)) ((_ extract 7 0) v))
+)
+(define-fun storefun_LE_32_8_64
+  ((a (Array (_ BitVec 32) (_ BitVec 8))) (ad (_ BitVec 32)) (v (_ BitVec 64)))
+  (Array (_ BitVec 32) (_ BitVec 8))
+  (store (store (store (store (store (store (store (store a (bvadd ad (_ bv7 32)) ((_ extract 63 56) v)) (bvadd ad (_ bv6 32)) ((_ extract 55 48) v)) (bvadd ad (_ bv5 32)) ((_ extract 47 40) v)) (bvadd ad (_ bv4 32)) ((_ extract 39 32) v)) (bvadd ad (_ bv3 32)) ((_ extract 31 24) v)) (bvadd ad (_ bv2 32)) ((_ extract 23 16) v)) (bvadd ad (_ bv1 32)) ((_ extract 15 8) v)) (bvadd ad (_ bv0 32)) ((_ extract 7 0) v))
+)
+
+; memory 64->8 (LE)
+; ----------------------
+(define-fun loadfun_LE_64_8_8
+  ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)))
+  (_ BitVec 8)
+  (select a ad)
+)
+(define-fun loadfun_LE_64_8_16
+  ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)))
+  (_ BitVec 16)
+  (concat (select a (bvadd ad (_ bv1 64))) (select a (bvadd ad (_ bv0 64))))
+)
+(define-fun loadfun_LE_64_8_32
+  ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)))
+  (_ BitVec 32)
+  (concat (select a (bvadd ad (_ bv3 64))) (select a (bvadd ad (_ bv2 64))) (select a (bvadd ad (_ bv1 64))) (select a (bvadd ad (_ bv0 64))))
+)
+(define-fun loadfun_LE_64_8_64
+  ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)))
+  (_ BitVec 64)
+  (concat (select a (bvadd ad (_ bv7 64))) (select a (bvadd ad (_ bv6 64))) (select a (bvadd ad (_ bv5 64))) (select a (bvadd ad (_ bv4 64))) (select a (bvadd ad (_ bv3 64))) (select a (bvadd ad (_ bv2 64))) (select a (bvadd ad (_ bv1 64))) (select a (bvadd ad (_ bv0 64))))
+)
+
+(define-fun storefun_LE_64_8_8
+  ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)) (v (_ BitVec 8)))
+  (Array (_ BitVec 64) (_ BitVec 8))
+  (store a ad v)
+)
+(define-fun storefun_LE_64_8_16
+  ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)) (v (_ BitVec 16)))
+  (Array (_ BitVec 64) (_ BitVec 8))
+  (store (store a (bvadd ad (_ bv1 64)) ((_ extract 15 8) v)) (bvadd ad (_ bv0 64)) ((_ extract 7 0) v))
+)
+(define-fun storefun_LE_64_8_32
+  ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)) (v (_ BitVec 32)))
+  (Array (_ BitVec 64) (_ BitVec 8))
+  (store (store (store (store a (bvadd ad (_ bv3 64)) ((_ extract 31 24) v)) (bvadd ad (_ bv2 64)) ((_ extract 23 16) v)) (bvadd ad (_ bv1 64)) ((_ extract 15 8) v)) (bvadd ad (_ bv0 64)) ((_ extract 7 0) v))
+)
+(define-fun storefun_LE_64_8_64
+  ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)) (v (_ BitVec 64)))
+  (Array (_ BitVec 64) (_ BitVec 8))
+  (store (store (store (store (store (store (store (store a (bvadd ad (_ bv7 64)) ((_ extract 63 56) v)) (bvadd ad (_ bv6 64)) ((_ extract 55 48) v)) (bvadd ad (_ bv5 64)) ((_ extract 47 40) v)) (bvadd ad (_ bv4 64)) ((_ extract 39 32) v)) (bvadd ad (_ bv3 64)) ((_ extract 31 24) v)) (bvadd ad (_ bv2 64)) ((_ extract 23 16) v)) (bvadd ad (_ bv1 64)) ((_ extract 15 8) v)) (bvadd ad (_ bv0 64)) ((_ extract 7 0) v))
+)
+
+; --------------------------------------------------------------------------------------------