From 45bf1e6918a1d6f6cc41908b8240decf21061070 Mon Sep 17 00:00:00 2001 From: Andreas Lindner Date: Wed, 28 Aug 2024 22:24:41 +0200 Subject: [PATCH] Make z3 prelude autogenerated and based on a set of easily adjustable parameters --- src/shared/smt/bir_smtlibLib.z3_prelude | 161 ------------------ src/shared/smt/holba_z3Lib.sml | 18 +- src/shared/smt/holba_z3Lib_prelude.z3 | 89 ++++++++++ .../smt/test-holba_z3Lib_preludez3_gen.sml | 107 ++++++++++++ 4 files changed, 208 insertions(+), 167 deletions(-) delete mode 100644 src/shared/smt/bir_smtlibLib.z3_prelude create mode 100644 src/shared/smt/holba_z3Lib_prelude.z3 create mode 100644 src/shared/smt/test-holba_z3Lib_preludez3_gen.sml diff --git a/src/shared/smt/bir_smtlibLib.z3_prelude b/src/shared/smt/bir_smtlibLib.z3_prelude deleted file mode 100644 index 4ab604a7f..000000000 --- a/src/shared/smt/bir_smtlibLib.z3_prelude +++ /dev/null @@ -1,161 +0,0 @@ -; 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)) -) - -; -------------------------------------------------------------------------------------------- diff --git a/src/shared/smt/holba_z3Lib.sml b/src/shared/smt/holba_z3Lib.sml index a8d2855a4..ffce4152f 100644 --- 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 new file mode 100644 index 000000000..b97ad7305 --- /dev/null +++ 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)) +) + +; -------------------------------------------------------------------------------------------- diff --git a/src/shared/smt/test-holba_z3Lib_preludez3_gen.sml b/src/shared/smt/test-holba_z3Lib_preludez3_gen.sml new file mode 100644 index 000000000..c3795ff40 --- /dev/null +++ b/src/shared/smt/test-holba_z3Lib_preludez3_gen.sml @@ -0,0 +1,107 @@ +open HolKernel Parse; + +open holba_fileLib; +open holba_z3Lib; + +(* +val endi = SMTMEM_LittleEndian; +val szadi = 32; +val szci = 8; +val szi = 16; +val opparam = (endi, szadi, szci, szi); +*) +val mem_params = (List.concat o List.map (fn szadi => (List.concat o List.map (fn szci => List.map (fn endi => (endi, szadi, szci)) gen_smt_as_funcall_endis)) gen_smt_as_funcall_szcis)) gen_smt_as_funcall_szadis; + +fun gen_type_array (endi, szadi, szci, szi) = + (SMTTY_ARR (szadi, szci)); +fun gen_type_address (endi, szadi, szci, szi) = + (SMTTY_BV szadi); +fun gen_type_value (endi, szadi, szci, szi) = + (SMTTY_BV szi); +fun gen_fun_param vn vt = + "(" ^ vn ^ " " ^ vt ^ ")"; + +fun gen_define_fun_load opparam = + let + val arrname = "a"; + val addname = "ad"; + val arrtype = gen_type_array opparam; + val addtype = gen_type_address opparam; + val valtype = gen_type_value opparam; + val valm = (arrname, arrtype); + val valad = (addname, addtype); + + val funname = gen_smt_loadstore_funname "load" opparam; + val params = "(" ^ gen_fun_param arrname (smt_type_to_smtlib arrtype) ^ + " " ^ gen_fun_param addname (smt_type_to_smtlib addtype) ^ ")"; + val rettype = smt_type_to_smtlib valtype; + val exp = fst (gen_smt_load_as_exp valm valad opparam); + in + "(define-fun " ^ funname ^ "\n" ^ + " " ^ params ^ "\n" ^ + " " ^ rettype ^ "\n" ^ + " " ^ exp ^ "\n" ^ + ")\n" + end; + +fun gen_define_fun_store opparam = + let + val arrname = "a"; + val addname = "ad"; + val valname = "v"; + val arrtype = gen_type_array opparam; + val addtype = gen_type_address opparam; + val valtype = gen_type_value opparam; + val valm = (arrname, arrtype); + val valad = (addname, addtype); + val valv = (valname, valtype); + + val funname = gen_smt_loadstore_funname "store" opparam; + val params = "(" ^ gen_fun_param arrname (smt_type_to_smtlib arrtype) ^ + " " ^ gen_fun_param addname (smt_type_to_smtlib addtype) ^ + " " ^ gen_fun_param valname (smt_type_to_smtlib valtype) ^ ")"; + val rettype = smt_type_to_smtlib arrtype; + val exp = fst (gen_smt_store_as_exp valm valad valv opparam); + in + "(define-fun " ^ funname ^ "\n" ^ + " " ^ params ^ "\n" ^ + " " ^ rettype ^ "\n" ^ + " " ^ exp ^ "\n" ^ + ")\n" + end; + +(* +val _ = print ("\n\n" ^ gen_define_fun_load opparam ^ "\n\n"); +val _ = print ("\n\n" ^ gen_define_fun_store opparam ^ "\n\n"); +*) + +val str = foldl (fn ((endi, szadi, szci), acc) => + let + fun genopparam szi = (endi, szadi, szci, szi); + + val str = ""; + val str = str ^ "; memory " ^ Int.toString szadi ^ "->" ^ Int.toString szci ^ " (" ^ bir_smt_mem_endianness_to_string endi ^ ")\n"; + val str = str ^ "; ----------------------\n"; + + val str = foldl (fn (szi,acc) => acc ^ (gen_define_fun_load (genopparam szi))) str gen_smt_as_funcall_szis; + val str = str ^ "\n"; + val str = foldl (fn (szi,acc) => acc ^ (gen_define_fun_store (genopparam szi))) str gen_smt_as_funcall_szis; + val str = str ^ "\n"; + in + acc ^ str + end +) "" mem_params; +val str = str ^ "; --------------------------------------------------------------------------------------------\n"; + +(* +val _ = print ("\n\n" ^ str ^ "\n\n"); +*) + +val _ = write_to_file "holba_z3Lib_prelude.z3" str; + +(* check whether the result is different *) +val _ = + if OS.Process.isSuccess (OS.Process.system ("git diff --exit-code holba_z3Lib_prelude.z3")) + then () + else + raise Fail ("test-holba_z3Lib_preludez3_gen::The generated z3 prelude is not the same as in the git repostioriy")