From 3f4706f07921ca23deaa45e09cf1e65aab6bdaff Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Wed, 6 Nov 2024 13:48:41 +0000 Subject: [PATCH 1/3] Update alt-ergo-lib pin version To play nicely with the installation of frama-c in Owi --- smtml.opam | 2 +- smtml.opam.template | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/smtml.opam b/smtml.opam index de0eb7b0..7b555581 100644 --- a/smtml.opam +++ b/smtml.opam @@ -68,7 +68,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"] - ["alt-ergo-lib.dev" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"] + ["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/filipeom/benchpress.git#50355de32835b12f1b065a4700f493bc3d8c5342"] ] diff --git a/smtml.opam.template b/smtml.opam.template index 0c3ff732..e5fbd6a6 100644 --- a/smtml.opam.template +++ b/smtml.opam.template @@ -2,7 +2,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"] - ["alt-ergo-lib.dev" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"] + ["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/filipeom/benchpress.git#50355de32835b12f1b065a4700f493bc3d8c5342"] ] From cbf9d38464c3343ba5bba99b9dfce97150cd245f Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Wed, 6 Nov 2024 14:34:59 +0000 Subject: [PATCH 2/3] Fixes incorrect type calculation of bitv `*_extend` ops --- src/ast/expr.ml | 3 ++- test/unit/dune | 1 + test/unit/test_ty.ml | 8 ++++++++ 3 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 test/unit/test_ty.ml diff --git a/src/ast/expr.ml b/src/ast/expr.ml index 67c9d368..f4519cb9 100644 --- a/src/ast/expr.ml +++ b/src/ast/expr.ml @@ -133,7 +133,8 @@ let rec ty (hte : t) : Ty.t = ty1 | Triop (ty, _, _, _, _) -> ty | Relop (ty, _, _, _) -> ty - | Cvtop (Ty_bitv n, (Zero_extend m | Sign_extend m), _) -> Ty_bitv (n + m) + | Cvtop (_, (Zero_extend m | Sign_extend m), hte) -> ( + match ty hte with Ty_bitv n -> Ty_bitv (n + m) | _ -> assert false ) | Cvtop (ty, _, _) -> ty | Naryop (ty, _, _) -> ty | Extract (_, h, l) -> Ty_bitv ((h - l) * 8) diff --git a/test/unit/dune b/test/unit/dune index fadc38a4..0ef40dec 100644 --- a/test/unit/dune +++ b/test/unit/dune @@ -5,6 +5,7 @@ test_unop test_binop test_triop + test_ty test_relop test_cvtop test_naryop diff --git a/test/unit/test_ty.ml b/test/unit/test_ty.ml new file mode 100644 index 00000000..210c6e88 --- /dev/null +++ b/test/unit/test_ty.ml @@ -0,0 +1,8 @@ +open Smtml + +let () = + let x = Expr.symbol (Symbol.make (Ty_bitv 32) "x") in + let x = Expr.extract x ~high:2 ~low:0 in + assert (Ty.equal (Expr.ty x) (Ty_bitv 16)); + let x = Expr.cvtop (Ty_bitv 32) (Sign_extend 16) x in + assert (Ty.equal (Expr.ty x) (Ty_bitv 32)) From e31fb754c41c99421cae4652554a38188ca0d104 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Wed, 6 Nov 2024 14:36:33 +0000 Subject: [PATCH 3/3] Update CHANGES.md --- CHANGES.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 4bfc11ec..eefda965 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,12 @@ ## Unreleased ### Added + ### Fixed + +- Fixes incorrect type calculation of bitv `*_extend` ops +- Bumps bitwuzla 0.4.0 -> 0.6.0 to fix segmentation faults + ### Changed ## v0.3.0