Add bitvector library

CHANGES.md

@@ -1,13 +1,26 @@
 ## Unreleased
 
 ### Added
-### Fixed
+
+- Add Bitvector library
+- optimize Expr.equal, cache Expr.simplify (@zapashcanon)
+- Add floating-point operator `Copysign` (Closes #185)
+- Add sign extension to operators with unsigned counter parts (Closes #207)
+
 ### Changed
 
+- Use bitvector library for bitvectors instead of `Num (IXX _)`
+
+### Fixed
+
+- Bring back forall and exists quantifiers (Closes #200)
+- Fixes `Value.compare` (Closes #210)
+
 ## v0.5.0
 
 ### Changed
 
+- Bump `prelude` 0.3 -> 0.5
 - Removes `satisfiability` type
 
 ## v0.4.1

bin/dune

@@ -1,4 +1,5 @@
 (executable
+ (package smtml)
  (name main)
  (public_name smtml)
  (libraries cmdliner smtml)

bitvector.opam

@@ -0,0 +1,39 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Another Arbitrary-Width Bitvectors using the Zarith Library"
+description: "Arbitrary-Width Bitvectors using the Zarith Library"
+maintainer: ["Filipe Marques <[email protected]>"]
+authors: [
+  "João Pereira <[email protected]>"
+  "Filipe Marques <[email protected]>"
+  "Hichem Rami Ait El Hara <[email protected]>"
+  "Léo Andrès <[email protected]>"
+  "Arthur Carcano <[email protected]>"
+  "Pierre Chambart <[email protected]>"
+  "José Fragoso Santos <[email protected]>"
+]
+license: "MIT"
+homepage: "https://github.com/formalsec/smtml"
+doc: "https://formalsec.github.io/smtml/smtml/index.html"
+bug-reports: "https://github.com/formalsec/smtml/issues"
+depends: [
+  "dune" {>= "3.10"}
+  "ocaml" {>= "4.14.0"}
+  "zarith"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/formalsec/smtml.git"

dune-project

@@ -26,6 +26,15 @@
 
 (license "MIT")
 
+(package
+ (name bitvector)
+ (synopsis "Another Arbitrary-Width Bitvectors using the Zarith Library")
+ (description "Arbitrary-Width Bitvectors using the Zarith Library")
+ (depends
+  (ocaml
+   (>= "4.14.0"))
+  zarith))
+
 (package
  (name smtml)
  (synopsis "An SMT solver frontend for OCaml")

smtml.opam

@@ -71,8 +71,8 @@ build: [
 dev-repo: "git+https://github.com/formalsec/smtml.git"
 available: arch != "arm32" & arch != "x86_32"
 pin-depends: [
-  ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"]
-  ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"]
+  ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"]
+  ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"]
   ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
   ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"]
   ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"]

smtml.opam.template

@@ -1,7 +1,7 @@
 available: arch != "arm32" & arch != "x86_32"
 pin-depends: [
-  ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"]
-  ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#1feba887bbb7980f27bbcec8137eb908caa8f0ce"]
+  ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"]
+  ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#e15e6fc52b1f4e9a015b630a1f377d203ed9ec5b"]
   ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
   ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"]
   ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"]

src/bisect.exclude

@@ -1,3 +1,3 @@
-file "src/colibri2_mappings.ml"
-file "src/bitwuzla_mappings.ml"
-file "src/cvc5_mappings.ml"
+file "src/smtml/colibri2_mappings.ml"
+file "src/smtml/bitwuzla_mappings.ml"
+file "src/smtml/cvc5_mappings.ml"

src/bitvector/bitvector.ml

@@ -0,0 +1,166 @@
+type t =
+  { value : Z.t
+  ; width : int
+  }
+
+let mask width = Z.pred (Z.shift_left Z.one width)
+
+let make v m =
+  let masked_value = Z.logand v (mask m) in
+  { value = masked_value; width = m }
+
+let view { value; _ } = value
+
+let numbits { width; _ } = width
+
+let equal a b = Z.equal a.value b.value && a.width = b.width
+
+let compare a b = Z.compare a.value b.value
+
+let msb bv = Z.testbit bv.value (bv.width - 1)
+
+let to_signed bv =
+  let msb = msb bv in
+  if msb then Z.sub bv.value (Z.shift_left Z.one bv.width) else bv.value
+
+let pp fmt bv = Z.pp_print fmt bv.value
+
+(* Unop *)
+let neg bv = make (Z.neg bv.value) bv.width
+
+let lognot a = make (Z.lognot a.value) a.width
+
+let clz bv =
+  let rec count_zeros i =
+    if i >= bv.width || Z.testbit bv.value (bv.width - 1 - i) then i
+    else count_zeros (i + 1)
+  in
+  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
+  make (Z.of_int @@ count_zeros 0) bv.width
+
+let popcnt bv = make (Z.of_int @@ Z.popcount bv.value) bv.width
+
+(* Binop *)
+let add a b =
+  assert (a.width = b.width);
+  make (Z.add a.value b.value) a.width
+
+let sub a b =
+  assert (a.width = b.width);
+  make (Z.sub a.value b.value) a.width
+
+let mul a b =
+  assert (a.width = b.width);
+  make (Z.mul a.value b.value) a.width
+
+let div a b =
+  assert (a.width = b.width);
+  if Z.equal b.value Z.zero then invalid_arg "division by zero";
+  make (Z.div (to_signed a) (to_signed b)) a.width
+
+let div_u a b =
+  assert (a.width = b.width);
+  if Z.equal b.value Z.zero then invalid_arg "division by zero";
+  make (Z.div a.value b.value) a.width
+
+let logand a b =
+  assert (a.width = b.width);
+  make (Z.logand a.value b.value) a.width
+
+let logor a b =
+  assert (a.width = b.width);
+  make (Z.logor a.value b.value) a.width
+
+let logxor a b =
+  assert (a.width = b.width);
+  make (Z.logxor a.value b.value) a.width
+
+let shl a n =
+  let n = Z.to_int n.value in
+  make (Z.shift_left a.value n) a.width
+
+let ashr a n =
+  let n = Z.to_int n.value in
+  let signed_value = to_signed a in
+  make (Z.shift_right signed_value n) a.width
+
+let lshr a n =
+  let n = Z.to_int n.value in
+  make (Z.shift_right_trunc a.value n) a.width
+
+let rem a b =
+  assert (a.width = b.width);
+  if Z.equal b.value Z.zero then invalid_arg "division by zero";
+  make (Z.rem (to_signed a) (to_signed b)) a.width
+
+let rem_u a b =
+  assert (a.width = b.width);
+  if Z.equal b.value Z.zero then invalid_arg "division by zero";
+  make (Z.rem a.value b.value) a.width
+
+let rotate_left bv n =
+  let n = Z.to_int n.value mod bv.width in
+  let left_part = Z.shift_left bv.value n in
+  let right_part = Z.shift_right bv.value (bv.width - n) in
+  let rotated = Z.logor left_part right_part in
+  make rotated bv.width
+
+let rotate_right bv n =
+  let n = Z.to_int n.value mod bv.width in
+  let right_part = Z.shift_right bv.value n in
+  let left_part = Z.shift_left bv.value (bv.width - n) in
+  let rotated = Z.logor left_part right_part in
+  make rotated bv.width
+
+(* Relop *)
+let lt_u a b = Z.lt a.value b.value
+
+let gt_u a b = Z.gt a.value b.value
+
+let le_u a b = Z.leq a.value b.value
+
+let ge_u a b = Z.geq a.value b.value
+
+let lt a b = Z.lt (to_signed a) (to_signed b)
+
+let gt a b = Z.gt (to_signed a) (to_signed b)
+
+let le a b = Z.leq (to_signed a) (to_signed b)
+
+let ge a b = Z.geq (to_signed a) (to_signed b)
+
+(* Extract and concat *)
+let concat a b =
+  let new_width = a.width + b.width in
+  let shifted = Z.shift_left a.value b.width in
+  let combined = Z.logor shifted b.value in
+  make combined new_width
+
+let extract bv ~high ~low =
+  assert (high <= bv.width && low >= 0 && low < high);
+  let width = high - low + 1 in
+  let shifted = Z.shift_right bv.value low in
+  let extracted = Z.logand shifted (mask width) in
+  make extracted width
+
+(* Cvtop *)
+let zero_extend width bv =
+  let new_width = bv.width + width in
+  make bv.value new_width
+
+let sign_extend width bv =
+  let new_width = bv.width + width in
+  let msb = msb bv in
+  let sign_mask =
+    if msb then
+      let shift_amount = bv.width in
+      Z.shift_left (mask width) shift_amount
+    else Z.zero
+  in
+  let extended = Z.logor bv.value sign_mask in
+  make extended new_width

src/bitvector/bitvector.mli

@@ -0,0 +1,77 @@
+type t
+
+val make : Z.t -> int -> t
+
+val view : t -> Z.t
+
+val numbits : t -> int
+
+val equal : t -> t -> bool
+
+val compare : t -> t -> int
+
+val pp : Format.formatter -> t -> unit
+
+val neg : t -> t
+
+val lognot : t -> t
+
+val clz : t -> t
+
+val ctz : t -> t
+
+val popcnt : t -> t
+
+val add : t -> t -> t
+
+val sub : t -> t -> t
+
+val mul : t -> t -> t
+
+val div : t -> t -> t
+
+val div_u : t -> t -> t
+
+val logand : t -> t -> t
+
+val logor : t -> t -> t
+
+val logxor : t -> t -> t
+
+val shl : t -> t -> t
+
+val ashr : t -> t -> t
+
+val lshr : t -> t -> t
+
+val rem : t -> t -> t
+
+val rem_u : t -> t -> t
+
+val rotate_left : t -> t -> t
+
+val rotate_right : t -> t -> t
+
+val lt : t -> t -> bool
+
+val lt_u : t -> t -> bool
+
+val gt : t -> t -> bool
+
+val gt_u : t -> t -> bool
+
+val le : t -> t -> bool
+
+val le_u : t -> t -> bool
+
+val ge : t -> t -> bool
+
+val ge_u : t -> t -> bool
+
+val concat : t -> t -> t
+
+val extract : t -> high:int -> low:int -> t
+
+val zero_extend : int -> t -> t
+
+val sign_extend : int -> t -> t

src/bitvector/dune

@@ -0,0 +1,6 @@
+(library
+ (wrapped false)
+ (name bitvector)
+ (public_name bitvector)
+ (modules bitvector)
+ (libraries zarith))