WIP

Author: filipeom

src/bitvector/bitvector.ml

@@ -35,15 +35,15 @@ let clz bv =
     if i >= bv.width || Z.testbit bv.value (bv.width - 1 - i) then i
     else count_zeros (i + 1)
   in
-  count_zeros 0
+  make (Z.of_int @@ count_zeros 0) bv.width
 
 let ctz bv =
   let rec count_zeros i =
     if i >= bv.width || Z.testbit bv.value i then i else count_zeros (i + 1)
   in
-  count_zeros 0
+  make (Z.of_int @@ count_zeros 0) bv.width
 
-let popcnt bv = Z.popcount bv.value
+let popcnt bv = make (Z.of_int @@ Z.popcount bv.value) bv.width
 
 (* Binop *)
 let add a b =

src/bitvector/bitvector.mli

@@ -16,11 +16,11 @@ val neg : t -> t
 
 val lognot : t -> t
 
-val clz : t -> int
+val clz : t -> t
 
-val ctz : t -> int
+val ctz : t -> t
 
-val popcnt : t -> int
+val popcnt : t -> t
 
 val add : t -> t -> t
 

src/smtml/dune

@@ -55,6 +55,7 @@
  (flags
   (:standard -open Smtml_prelude))
  (libraries
+  bitvector
   bos
   cmdliner
   dolmen

src/smtml/eval.ml

@@ -439,6 +439,65 @@ module Lst = struct
       Fmt.failwith {|naryop: Unsupported list operator "%a"|} Ty.Naryop.pp op
 end
 
+module Bitv = struct
+  let to_value (bv : Bitvector.t) : Value.t = Bitv bv [@@inline]
+
+  let of_value (n : int) (op : op_type) (v : Value.t) =
+    of_arg
+      (function Bitv bv -> bv | _ -> raise_notrace (Value (Ty_bitv 0)))
+      n v op
+  [@@inline]
+
+  let unop (op : Ty.Unop.t) (v : Value.t) : Value.t =
+    let f =
+      match op with
+      | Neg -> Bitvector.neg
+      | Not -> Bitvector.lognot
+      | Clz -> Bitvector.clz
+      | Ctz -> Bitvector.ctz
+      | _ -> Fmt.failwith {|unop: Unsupported i32 operator "%a"|} Ty.Unop.pp op
+    in
+    to_value (f (of_value 1 (`Unop op) v))
+
+  let binop op v1 v2 =
+    let f =
+      match op with
+      | Ty.Binop.Add -> Bitvector.add
+      | Sub -> Bitvector.sub
+      | Mul -> Bitvector.mul
+      | Div -> Bitvector.div
+      | DivU -> Bitvector.div_u
+      | Rem -> Bitvector.rem
+      | RemU -> Bitvector.rem_u
+      | And -> Bitvector.logand
+      | Or -> Bitvector.logor
+      | Xor -> Bitvector.logxor
+      | Shl -> Bitvector.shl
+      | ShrL -> Bitvector.lshr
+      | ShrA -> Bitvector.ashr
+      | Rotl -> Bitvector.rotate_left
+      | Rotr -> Bitvector.rotate_right
+      | _ ->
+        Fmt.failwith {|binop: Unsupported i32 operator "%a"|} Ty.Binop.pp op
+    in
+    to_value (f (of_value 1 (`Binop op) v1) (of_value 2 (`Binop op) v2))
+
+  let relop (op : Ty.Relop.t) (v1 : Value.t) (v2 : Value.t) : bool =
+    let f =
+      match op with
+      | Lt -> Bitvector.lt
+      | LtU -> Bitvector.lt_u
+      | Le -> Bitvector.le
+      | LeU -> Bitvector.le_u
+      | Gt -> Bitvector.gt
+      | GtU -> Bitvector.gt_u
+      | Ge -> Bitvector.ge
+      | GeU -> Bitvector.ge_u
+      | Eq | Ne -> assert false
+    in
+    f (of_value 1 (`Relop op) v1) (of_value 2 (`Relop op) v2)
+end
+
 module I32 = struct
   let to_value (i : int32) : Value.t = Num (I32 i) [@@inline]
 

src/smtml/mappings.ml

@@ -547,6 +547,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Num (I64 x) -> I64.v x
       | Num (F32 x) -> Float32_impl.v x
       | Num (F64 x) -> Float64_impl.v x
+      | Bitv _bv -> assert false
       | List _ | App _ | Unit | Nothing -> assert false
 
     let unop = function

src/smtml/value.ml

@@ -12,6 +12,7 @@ type t =
   | Real of float
   | Str of string
   | Num of Num.t
+  | Bitv of Bitvector.t
   | List of t list
   | App : [> `Op of string ] * t list -> t
   | Nothing
@@ -24,6 +25,7 @@ let type_of (v : t) : Ty.t =
   | Real _ -> Ty_real
   | Str _ -> Ty_str
   | Num n -> Num.type_of n
+  | Bitv bv -> Ty_bitv (Bitvector.numbits bv)
   | List _ -> Ty_list
   | App _ -> Ty_app
   | Nothing -> Ty_none
@@ -36,9 +38,10 @@ let discr = function
   | Real _ -> 4
   | Str _ -> 5
   | Num _ -> 6
-  | List _ -> 7
-  | App _ -> 8
-  | Nothing -> 9
+  | Bitv _ -> 7
+  | List _ -> 8
+  | App _ -> 9
+  | Nothing -> 10
 
 let rec compare (a : t) (b : t) : int =
   match (a, b) with
@@ -49,28 +52,30 @@ let rec compare (a : t) (b : t) : int =
   | Real a, Real b -> Float.compare a b
   | Str a, Str b -> String.compare a b
   | Num a, Num b -> Num.compare a b
+  | Bitv a, Bitv b -> Bitvector.compare a b
   | List a, List b -> List.compare compare a b
   | App (`Op op1, vs1), App (`Op op2, vs2) ->
     let c = String.compare op1 op2 in
     if c = 0 then List.compare compare vs1 vs2 else c
-  | ( ( True | False | Unit | Int _ | Real _ | Str _ | Num _ | List _ | App _
-      | Nothing )
+  | ( ( True | False | Unit | Int _ | Real _ | Str _ | Num _ | Bitv _ | List _
+      | App _ | Nothing )
     , _ ) ->
     (* TODO: I don't know if this is always semantically correct *)
     Int.compare (discr a) (discr b)
 
 let rec equal (v1 : t) (v2 : t) : bool =
   match (v1, v2) with
   | True, True | False, False | Unit, Unit | Nothing, Nothing -> true
-  | Int x1, Int x2 -> Int.equal x1 x2
-  | Real x1, Real x2 -> Float.equal x1 x2
-  | Str x1, Str x2 -> String.equal x1 x2
-  | Num x1, Num x2 -> Num.equal x1 x2
+  | Int a, Int b -> Int.equal a b
+  | Real a, Real b -> Float.equal a b
+  | Str a, Str b -> String.equal a b
+  | Num a, Num b -> Num.equal a b
+  | Bitv a, Bitv b -> Bitvector.equal a b
   | List l1, List l2 -> List.equal equal l1 l2
   | App (`Op op1, vs1), App (`Op op2, vs2) ->
     String.equal op1 op2 && List.equal equal vs1 vs2
-  | ( ( True | False | Unit | Int _ | Real _ | Str _ | Num _ | List _ | App _
-      | Nothing )
+  | ( ( True | False | Unit | Int _ | Real _ | Str _ | Num _ | Bitv _ | List _
+      | App _ | Nothing )
     , _ ) ->
     false
 
@@ -85,6 +90,7 @@ let rec pp fmt = function
   | Int x -> Fmt.int fmt x
   | Real x -> Fmt.pf fmt "%F" x
   | Num x -> Num.pp_no_type fmt x
+  | Bitv x -> Bitvector.pp fmt x
   | Str x -> Fmt.pf fmt "%S" x
   | List l -> (Fmt.hovbox ~indent:1 (Fmt.list ~sep:Fmt.comma pp)) fmt l
   | App (`Op op, vs) ->
@@ -126,6 +132,7 @@ let rec to_json (v : t) : Yojson.Basic.t =
   | Real real -> `Float real
   | Str str -> `String str
   | Num n -> Num.to_json n
+  | Bitv bv -> `String (Fmt.str "%a" Bitvector.pp bv)
   | List l -> `List (List.map to_json l)
   | Nothing -> `Null
   | App _ -> assert false

src/smtml/value.mli

@@ -10,6 +10,7 @@ type t =
   | Real of float
   | Str of string
   | Num of Num.t
+  | Bitv of Bitvector.t
   | List of t list
   | App : [> `Op of string ] * t list -> t
   | Nothing