Fixes incorrect type calculation of bitv *_extend ops

formalsec · Nov 6, 2024 · f46d245 · f46d245
1 parent 8f5d2c8
commit f46d245
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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))