Allow creating and lifting bitvecs with bw = 1

formalsec · Jul 18, 2024 · 2c18703 · 2c18703
1 parent 9070d32
commit 2c18703
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 2 deletions.
diff --git a/lib/mappings.ml b/lib/mappings.ml
@@ -61,9 +61,10 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty_bitv 8 -> i8
       | Ty_bitv 32 -> i32
       | Ty_bitv 64 -> i64
+      | Ty_bitv n -> M.Types.bitv n
       | Ty_fp 32 -> f32
       | Ty_fp 64 -> f64
-      | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit -> assert false
+      | Ty_fp _ | Ty_list | Ty_app | Ty_unit -> assert false
 
     let make_symbol (symbol_table : sym_tbl) (s : Symbol.t) : M.term =
       match Hashtbl.find_opt symbol_table s with
@@ -590,6 +591,12 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty_str ->
         let str = M.Interp.to_string v in
         Value.Str str
+      | Ty_bitv 1 ->
+        let b = M.Interp.to_bitv v 1 in
+        if b = 1L then Value.True
+        else (
+          assert (b = 0L);
+          Value.False )
       | Ty_bitv 8 ->
         let i8 = M.Interp.to_bitv v 8 in
         Value.Num (I8 (Int64.to_int i8))

diff --git a/lib/z3_mappings.default.ml b/lib/z3_mappings.default.ml
@@ -69,9 +69,10 @@ module Fresh = struct
       | Ty_bitv 8 -> bv8_sort
       | Ty_bitv 32 -> bv32_sort
       | Ty_bitv 64 -> bv64_sort
+      | Ty_bitv n -> Z3.BitVector.mk_sort ctx n
       | Ty_fp 32 -> fp32_sort
       | Ty_fp 64 -> fp64_sort
-      | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit -> assert false
+      | Ty_fp _ | Ty_list | Ty_app | Ty_unit -> assert false
 
     module Arithmetic = struct
       open Ty
@@ -788,6 +789,13 @@ module Fresh = struct
           (* It can never be something else *)
           assert false )
       | Ty_str, Z3enums.SEQ_SORT -> Str (Z3.Seq.get_string ctx e)
+      | Ty_bitv 1, Z3enums.BV_SORT ->
+        (* Hack: properly represent values with bitwidth = 1 *)
+        let bit = int64_of_bv e in
+        if bit = 1L then True
+        else (
+          assert (bit = 0L);
+          False )
       | Ty_bitv 8, Z3enums.BV_SORT -> Num (I8 (Int64.to_int (int64_of_bv e)))
       | Ty_bitv 32, Z3enums.BV_SORT -> Num (I32 (Int64.to_int32 (int64_of_bv e)))
       | Ty_bitv 64, Z3enums.BV_SORT -> Num (I64 (int64_of_bv e))