From bee3702580b8fdf6a3bdbe586dc30e5126020b52 Mon Sep 17 00:00:00 2001 From: Michael McLoughlin Date: Wed, 1 Nov 2023 11:16:53 -0400 Subject: [PATCH] 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 https://github.com/Z3Prover/z3/pull/6715 --- cranelift/isle/isle/src/ast.rs | 16 +++-- cranelift/isle/isle/src/parser.rs | 72 ++++++++++++------- .../isle/veri/veri_engine/src/annotations.rs | 1 + cranelift/isle/veri/veri_engine/src/solver.rs | 1 + .../veri/veri_engine/src/type_inference.rs | 16 +++++ .../isle/veri/veri_ir/src/annotation_ir.rs | 3 + cranelift/isle/veri/veri_ir/src/lib.rs | 2 + 7 files changed, 78 insertions(+), 33 deletions(-) diff --git a/cranelift/isle/isle/src/ast.rs b/cranelift/isle/isle/src/ast.rs index 6d64be930312..c7bdfeea8099 100644 --- a/cranelift/isle/isle/src/ast.rs +++ b/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, 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, } - /// 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) + BitVec(Option), } /// A construct's value in SMT-LIB diff --git a/cranelift/isle/isle/src/parser.rs b/cranelift/isle/isle/src/parser.rs index c9528a27c461..4cb2a08c72c9 100644 --- a/cranelift/isle/isle/src/parser.rs +++ b/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,6 +475,7 @@ 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), @@ -479,7 +483,7 @@ impl<'a> Parser<'a> { "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 { @@ -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(), + )) } } diff --git a/cranelift/isle/veri/veri_engine/src/annotations.rs b/cranelift/isle/veri/veri_engine/src/annotations.rs index 366978b29cb9..6067c5443492 100644 --- a/cranelift/isle/veri/veri_engine/src/annotations.rs +++ b/cranelift/isle/veri/veri_engine/src/annotations.rs @@ -142,6 +142,7 @@ fn spec_op_to_expr(s: &SpecOp, args: &Vec, 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), diff --git a/cranelift/isle/veri/veri_engine/src/solver.rs b/cranelift/isle/veri/veri_engine/src/solver.rs index c7b0ef439d4d..1692363515e2 100644 --- a/cranelift/isle/veri/veri_engine/src/solver.rs +++ b/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 diff --git a/cranelift/isle/veri/veri_engine/src/type_inference.rs b/cranelift/isle/veri/veri_engine/src/type_inference.rs index 46b4ab7ff407..0fa814331d26 100644 --- a/cranelift/isle/veri/veri_engine/src/type_inference.rs +++ b/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); diff --git a/cranelift/isle/veri/veri_ir/src/annotation_ir.rs b/cranelift/isle/veri/veri_ir/src/annotation_ir.rs index 044ff2e733c6..79a7bdc6a788 100644 --- a/cranelift/isle/veri/veri_ir/src/annotation_ir.rs +++ b/cranelift/isle/veri/veri_ir/src/annotation_ir.rs @@ -179,6 +179,8 @@ pub enum Expr { BVUlt(Box, Box, u32), BVUlte(Box, Box, u32), + BVSaddo(Box, Box, 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) diff --git a/cranelift/isle/veri/veri_ir/src/lib.rs b/cranelift/isle/veri/veri_ir/src/lib.rs index 94276cff8478..c43a60b6d85f 100644 --- a/cranelift/isle/veri/veri_ir/src/lib.rs +++ b/cranelift/isle/veri/veri_ir/src/lib.rs @@ -175,6 +175,8 @@ pub enum BinaryOp { BVShl, BVShr, BVAShr, + + BVSaddo, } /// Expressions (combined across all types).