cranelift/isle/veri: add bvsaddo spec operation (#75)

Adds the `bvsaddo` SMT-LIB operator.

This operator is due to be standardized in SMT-LIB 2.7, and is already supported in Z3.

https://groups.google.com/g/smt-lib/c/J4D99wT0aKI
Z3Prover/z3#6715

cranelift/isle/isle/src/ast.rs

@@ -116,7 +116,7 @@ pub enum SpecExpr {
     },
     /// An application of a type variant or term.
     Op {
-        op: SpecOp, 
+        op: SpecOp,
         args: Vec<SpecExpr>,
         pos: Pos,
     },
@@ -128,7 +128,7 @@ pub enum SpecExpr {
     /// Enums variant values (enums defined by model)
     Enum {
         name: Ident,
-    }
+    },
 }
 
 /// An operation used to specify term semantics, similar to SMT-LIB syntax.
@@ -173,9 +173,12 @@ pub enum SpecOp {
     BVSlt,
     BVSle,
     BVSgt,
-    BVSge, 
+    BVSge,
 
-    // Desugared bitvector arithmetic operations 
+    // Bitvector overflow checks (SMT-LIB pending standardization)
+    BVSaddo,
+
+    // Desugared bitvector arithmetic operations
     Rotr,
     Rotl,
     Extract,
@@ -214,16 +217,15 @@ pub struct Spec {
     pub requires: Vec<SpecExpr>,
 }
 
-
 /// A model of an SMT-LIB type.
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub enum ModelType {
     /// SMT-LIB Int
-    Int, 
+    Int,
     /// SMT-LIB Int
     Bool,
     /// SMT-LIB bitvector, but with a potentially-polymorphic width
-    BitVec(Option<usize>)
+    BitVec(Option<usize>),
 }
 
 /// A construct's value in SMT-LIB

cranelift/isle/isle/src/parser.rs

@@ -413,7 +413,7 @@ impl<'a> Parser<'a> {
             let var = self.parse_ident()?;
             Ok(SpecExpr::Var { var, pos })
         } else if self.is_lparen() {
-            // TODO AVH: 
+            // TODO AVH:
             self.expect_lparen()?;
             if self.is_sym() && !self.is_spec_bit_vector() {
                 let sym = self.expect_symbol()?;
@@ -423,18 +423,21 @@ impl<'a> Parser<'a> {
                         args.push(self.parse_spec_expr()?);
                     }
                     self.expect_rparen()?;
-                    return Ok(SpecExpr::Op { op, args, pos })
+                    return Ok(SpecExpr::Op { op, args, pos });
                 };
                 let ident = self.str_to_ident(pos, &sym)?;
                 if self.is_rparen() {
                     self.expect_rparen()?;
-                    return Ok(SpecExpr::Enum { name: ident })
+                    return Ok(SpecExpr::Enum { name: ident });
                 };
-                // AVH TODO: see if we can simplify this to not backtrack, maybe 
-                // kill pairs 
+                // AVH TODO: see if we can simplify this to not backtrack, maybe
+                // kill pairs
                 let r = Box::new(self.parse_spec_expr()?);
                 self.expect_rparen()?;
-                Ok(SpecExpr::Pair { l: Box::new(SpecExpr::Var { var: ident, pos }), r })
+                Ok(SpecExpr::Pair {
+                    l: Box::new(SpecExpr::Var { var: ident, pos }),
+                    r,
+                })
             } else {
                 let l = Box::new(self.parse_spec_expr()?);
                 let r = Box::new(self.parse_spec_expr()?);
@@ -472,14 +475,15 @@ impl<'a> Parser<'a> {
             "bvshl" => Ok(SpecOp::BVShl),
             "bvlshr" => Ok(SpecOp::BVLshr),
             "bvashr" => Ok(SpecOp::BVAshr),
+            "bvsaddo" => Ok(SpecOp::BVSaddo),
             "bvule" => Ok(SpecOp::BVUle),
             "bvult" => Ok(SpecOp::BVUlt),
             "bvugt" => Ok(SpecOp::BVUgt),
             "bvuge" => Ok(SpecOp::BVUge),
             "bvslt" => Ok(SpecOp::BVSlt),
             "bvsle" => Ok(SpecOp::BVSle),
             "bvsgt" => Ok(SpecOp::BVSgt),
-            "bvsge" => Ok(SpecOp::BVSge), 
+            "bvsge" => Ok(SpecOp::BVSge),
             "rotr" => Ok(SpecOp::Rotr),
             "rotl" => Ok(SpecOp::Rotl),
             "extract" => Ok(SpecOp::Extract),
@@ -492,11 +496,11 @@ impl<'a> Parser<'a> {
             "widthof" => Ok(SpecOp::WidthOf),
             "if" => Ok(SpecOp::If),
             "switch" => Ok(SpecOp::Switch),
-            "subs"=> Ok(SpecOp::Subs),
-            "popcnt"=> Ok(SpecOp::Popcnt),
-            "rev"=> Ok(SpecOp::Rev),
-            "cls"=> Ok(SpecOp::Cls),
-            "clz"=> Ok(SpecOp::Clz),
+            "subs" => Ok(SpecOp::Subs),
+            "popcnt" => Ok(SpecOp::Popcnt),
+            "rev" => Ok(SpecOp::Rev),
+            "cls" => Ok(SpecOp::Cls),
+            "clz" => Ok(SpecOp::Clz),
             x => Err(self.error(pos, format!("Not a valid spec operator: {x}"))),
         }
     }
@@ -546,21 +550,35 @@ impl<'a> Parser<'a> {
             let mut implicit_idx = None;
 
             while !self.is_rparen() {
-                self.expect_lparen()?; // enum value 
+                self.expect_lparen()?; // enum value
                 let name = self.parse_ident()?;
-                let val = if self.is_rparen() { // has implicit enum value
+                let val = if self.is_rparen() {
+                    // has implicit enum value
                     if has_explicit_value {
-                        return Err(self.error(pos, format!("Spec enum has unexpected implicit value after implicit value.")));
+                        return Err(self.error(
+                            pos,
+                            format!(
+                                "Spec enum has unexpected implicit value after implicit value."
+                            ),
+                        ));
                     }
                     implicit_idx = Some(if let Some(idx) = implicit_idx {
                         idx + 1
                     } else {
                         0
                     });
-                    SpecExpr::ConstInt { val: implicit_idx.unwrap(), pos, }
+                    SpecExpr::ConstInt {
+                        val: implicit_idx.unwrap(),
+                        pos,
+                    }
                 } else {
                     if implicit_idx.is_some() {
-                        return Err(self.error(pos, format!("Spec enum has unexpected explicit value after implicit value.")));
+                        return Err(self.error(
+                            pos,
+                            format!(
+                                "Spec enum has unexpected explicit value after implicit value."
+                            ),
+                        ));
                     }
                     has_explicit_value = true;
                     self.parse_spec_expr()?
@@ -570,14 +588,11 @@ impl<'a> Parser<'a> {
             }
             ModelValue::EnumValues(variants)
         } else {
-            return Err(self.error(pos, "Model must be a type or enum".to_string()))
+            return Err(self.error(pos, "Model must be a type or enum".to_string()));
         };
 
         self.expect_rparen()?; // end body
-        Ok(Model{
-            name,
-            val,
-        })
+        Ok(Model { name, val })
     }
 
     fn parse_model_type(&mut self) -> Result<ModelType> {
@@ -592,17 +607,22 @@ impl<'a> Parser<'a> {
                 if self.is_rparen() {
                     None
                 } else if self.is_int() {
-                    Some(usize::try_from(self.expect_int()?).map_err(|err| self.error(pos, format!("Invalid BitVector width: {}", err)))?)
+                    Some(usize::try_from(self.expect_int()?).map_err(|err| {
+                        self.error(pos, format!("Invalid BitVector width: {}", err))
+                    })?)
                 } else {
-                    return Err(self.error(pos, "Badly formed BitVector (bv ...)".to_string()))
+                    return Err(self.error(pos, "Badly formed BitVector (bv ...)".to_string()));
                 }
             } else {
-                return Err(self.error(pos, "Badly formed BitVector (bv ...)".to_string()))
+                return Err(self.error(pos, "Badly formed BitVector (bv ...)".to_string()));
             };
             self.expect_rparen()?;
             Ok(ModelType::BitVec(width))
         } else {
-            Err(self.error(pos, "Model type be a Bool, Int, or BitVector (bv ...)".to_string()))
+            Err(self.error(
+                pos,
+                "Model type be a Bool, Int, or BitVector (bv ...)".to_string(),
+            ))
         }
     }
 

cranelift/isle/veri/veri_engine/src/annotations.rs

@@ -142,6 +142,7 @@ fn spec_op_to_expr(s: &SpecOp, args: &Vec<SpecExpr>, pos: &Pos, env: &ParsingEnv
         SpecOp::BVShl => binop(|x, y, i| Expr::BVShl(x, y, i), args, pos, env),
         SpecOp::BVLshr => binop(|x, y, i| Expr::BVShr(x, y, i), args, pos, env),
         SpecOp::BVAshr => binop(|x, y, i| Expr::BVAShr(x, y, i), args, pos, env),
+        SpecOp::BVSaddo => binop(|x, y, i| Expr::BVSaddo(x, y, i), args, pos, env),
         SpecOp::BVUle => binop(|x, y, i| Expr::BVUlte(x, y, i), args, pos, env),
         SpecOp::BVUlt => binop(|x, y, i| Expr::BVUlt(x, y, i), args, pos, env),
         SpecOp::BVUgt => binop(|x, y, i| Expr::BVUgt(x, y, i), args, pos, env),

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

@@ -799,6 +799,7 @@ impl SolverCtx {
                     BinaryOp::BVOr => "bvor",
                     BinaryOp::BVXor => "bvxor",
                     BinaryOp::BVShl => "bvshl",
+                    BinaryOp::BVSaddo => "bvsaddo",
                     _ => unreachable!("{:?}", op),
                 };
                 // If we have some static width that isn't the bitwidth, extract based on it

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

@@ -639,6 +639,22 @@ fn add_annotation_constraints(
             )
         }
 
+        annotation_ir::Expr::BVSaddo(x, y, _) => {
+            let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
+            let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
+            let t = tree.next_type_var;
+
+            tree.concrete_constraints
+                .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
+            tree.var_constraints.insert(TypeExpr::Variable(t1, t2));
+
+            tree.next_type_var += 1;
+            (
+                veri_ir::Expr::Binary(veri_ir::BinaryOp::BVSaddo, Box::new(e1), Box::new(e2)),
+                t,
+            )
+        }
+
         annotation_ir::Expr::BVNeg(x, _) => {
             let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
 

cranelift/isle/veri/veri_ir/src/annotation_ir.rs

@@ -179,6 +179,8 @@ pub enum Expr {
     BVUlt(Box<Expr>, Box<Expr>, u32),
     BVUlte(Box<Expr>, Box<Expr>, u32),
 
+    BVSaddo(Box<Expr>, Box<Expr>, u32),
+
     // Bitvector operations
     //      Note: these follow the naming conventions of the SMT theory of bitvectors:
     //      https://SMT-LIB.cs.uiowa.edu/version1/logics/QF_BV.smt
@@ -303,6 +305,7 @@ impl Expr {
             | Expr::BVShl(_, _, t)
             | Expr::BVShr(_, _, t)
             | Expr::BVAShr(_, _, t)
+            | Expr::BVSaddo(_, _, t)
             | Expr::Lt(_, _, t)
             | Expr::BVZeroExtTo(_, _, t)
             | Expr::BVZeroExtToVarWidth(_, _, t)

cranelift/isle/veri/veri_ir/src/lib.rs

@@ -175,6 +175,8 @@ pub enum BinaryOp {
     BVShl,
     BVShr,
     BVAShr,
+
+    BVSaddo,
 }
 
 /// Expressions (combined across all types).