spec: int2bv width can be an expression (bytecodealliance#136)

Updates the `int2bv` operator so its width can be an expression.

The current behavior was problematic in bytecodealliance#135, where it prevents the use
of `int2bv` in a macro expansion.

This PR brings `int2bv` in line with other operators taking an integer
width, such as zero extension.

cranelift/isle/veri/veri/src/solver.rs

@@ -211,7 +211,7 @@ impl<'a> Solver<'a> {
             Expr::BVConvTo(w, x) => self.bv_conv_to(w, x),
             Expr::BVExtract(h, l, x) => Ok(self.extract(h, l, self.expr_atom(x))),
             Expr::BVConcat(x, y) => Ok(self.smt.concat(self.expr_atom(x), self.expr_atom(y))),
-            Expr::Int2BV(w, x) => Ok(self.int2bv(w, self.expr_atom(x))),
+            Expr::Int2BV(w, x) => self.int_to_bv(w, x),
             Expr::WidthOf(x) => self.width_of(x),
         }
     }
@@ -303,6 +303,19 @@ impl<'a> Solver<'a> {
         }
     }
 
+    fn int_to_bv(&self, w: ExprId, x: ExprId) -> Result<SExpr> {
+        // Destination width expression should have known integer value.
+        let width: usize = self
+            .assignment
+            .try_int_value(w)
+            .context("destination width of int2bv expression should have known integer value")?
+            .try_into()
+            .expect("width should be representable as usize");
+
+        // Build int2bv expression.
+        Ok(self.int2bv(width, self.expr_atom(x)))
+    }
+
     fn width_of(&self, x: ExprId) -> Result<SExpr> {
         // QUESTION(mbm): should width_of expressions be elided or replaced after type inference?
 

cranelift/isle/veri/veri/src/spec.rs

@@ -95,7 +95,7 @@ pub enum Expr {
     BVConcat(Box<Expr>, Box<Expr>),
 
     // Convert integer to bitvector.
-    Int2BV(usize, Box<Expr>),
+    Int2BV(Box<Expr>, Box<Expr>),
 
     //// Convert bitvector to integer
     //BVToInt(Box<Expr>),
@@ -258,18 +258,7 @@ impl Expr {
                         Box::new(Expr::from_ast(&args[2])),
                     )
                 }
-                SpecOp::Int2BV => {
-                    // TODO(mbm): return error instead of assert
-                    assert_eq!(
-                        args.len(),
-                        2,
-                        "Unexpected number of args for int2bv operator at {pos:?}",
-                    );
-                    Expr::Int2BV(
-                        spec_expr_to_usize(&args[0]).unwrap(),
-                        Box::new(Expr::from_ast(&args[1])),
-                    )
-                }
+                SpecOp::Int2BV => binary_expr!(Expr::Int2BV, args, pos),
                 //SpecOp::Subs => {
                 //    assert_eq!(
                 //        args.len(),

cranelift/isle/veri/veri/src/type_inference.rs

@@ -391,8 +391,10 @@ impl<'a> SystemBuilder<'a> {
                 self.concat(x, *y, *z);
             }
             Expr::Int2BV(w, y) => {
-                self.bit_vector_of_width(x, *w);
+                self.bit_vector(x);
+                self.integer(*w);
                 self.integer(*y);
+                self.width_of(x, *w);
             }
             Expr::WidthOf(y) => {
                 self.integer(x);

cranelift/isle/veri/veri/src/veri.rs

@@ -80,7 +80,7 @@ pub enum Expr {
     BVConcat(ExprId, ExprId),
 
     // Integer conversion.
-    Int2BV(usize, ExprId),
+    Int2BV(ExprId, ExprId),
 
     // Bitwidth.
     WidthOf(ExprId),
@@ -172,7 +172,7 @@ impl std::fmt::Display for Expr {
             Self::BVConvTo(w, x) => write!(f, "bv_conv_to({}, {})", w.index(), x.index()),
             Self::BVExtract(h, l, x) => write!(f, "bv_extract({h}, {l}, {})", x.index()),
             Self::BVConcat(x, y) => write!(f, "bv_concat({}, {})", x.index(), y.index()),
-            Self::Int2BV(w, x) => write!(f, "int2bv({w}, {})", x.index()),
+            Self::Int2BV(w, x) => write!(f, "int2bv({}, {})", w.index(), x.index()),
             Self::WidthOf(x) => write!(f, "width_of({})", x.index()),
         }
     }
@@ -1361,8 +1361,9 @@ impl<'a> ConditionsBuilder<'a> {
             }
 
             spec::Expr::Int2BV(w, x) => {
+                let w = self.spec_expr(w, vars)?.try_into()?;
                 let x = self.spec_expr(x, vars)?.try_into()?;
-                Ok(self.scalar(Expr::Int2BV(*w, x)))
+                Ok(self.scalar(Expr::Int2BV(w, x)))
             }
 
             spec::Expr::WidthOf(x) => {