spec: type qualifier expression (bytecodealliance#171)

Add a spec expression `(as <expr> <ty>)` to specify the type of a spec
expression inline. The syntax is motivated by SMT-LIB qualified
identifiers.

The motivation for this is the need to express register width
constraints in ASLp-derived specs.

cranelift/isle/isle/build.rs

@@ -28,6 +28,7 @@ fn isle_printer_tests(out_dir: &std::path::PathBuf) {
     let mut out = String::new();
 
     emit_tests(&mut out, "isle_examples/pass", "run_print");
+    emit_tests(&mut out, "../veri/veri/filetests/pass", "run_print");
     emit_tests(&mut out, "../../codegen/src", "run_print");
     emit_tests(&mut out, "../../codegen/src/opts", "run_print");
     emit_tests(&mut out, "../../codegen/src/isa/x64", "run_print");

cranelift/isle/isle/src/ast.rs

@@ -149,6 +149,13 @@ pub enum SpecExpr {
         var: Ident,
         pos: Pos,
     },
+    // As expression specifies the intended type of the expression. Functionally
+    // it is the identity. Analogous to qualified identifiers in SMT-LIB.
+    As {
+        x: Box<SpecExpr>,
+        ty: ModelType,
+        pos: Pos,
+    },
     /// Struct field access.
     Field {
         field: Ident,
@@ -213,6 +220,7 @@ impl SpecExpr {
             | &Self::ConstBitVec { pos, .. }
             | &Self::ConstBool { pos, .. }
             | &Self::Var { pos, .. }
+            | &Self::As { pos, .. }
             | &Self::Field { pos, .. }
             | &Self::Discriminator { pos, .. }
             | &Self::Op { pos, .. }

cranelift/isle/isle/src/parser.rs

@@ -543,6 +543,11 @@ impl<'a> Parser<'a> {
                 }
                 self.expect_rparen()?;
                 Ok(SpecExpr::Match { x, arms, pos })
+            } else if self.eat_sym_str("as")? {
+                let x = Box::new(self.parse_spec_expr()?);
+                let ty = self.parse_model_type()?;
+                self.expect_rparen()?;
+                Ok(SpecExpr::As { x, ty, pos })
             } else if self.is_sym() && !self.is_spec_bit_vector() {
                 let sym_pos = self.pos();
                 let sym = self.expect_symbol()?;

cranelift/isle/isle/src/printer.rs

@@ -240,6 +240,9 @@ impl Printable for SpecExpr {
             }),
             SpecExpr::ConstBool { val, .. } => RcDoc::text(if *val { "true" } else { "false" }),
             SpecExpr::Var { var, .. } => var.to_doc(),
+            SpecExpr::As { x, ty, pos: _ } => {
+                sexp(vec![RcDoc::text("as"), x.to_doc(), ty.to_doc()])
+            }
             SpecExpr::Op { op, args, .. } => sexp(
                 Vec::from([op.to_doc()])
                     .into_iter()

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

@@ -302,6 +302,11 @@ pub fn substitute(expr: SpecExpr, substitutions: &HashMap<String, SpecExpr>) ->
         }
 
         // Recurse into child expressions.
+        SpecExpr::As { x, ty, pos } => SpecExpr::As {
+            x: Box::new(substitute(*x, substitutions)?),
+            ty,
+            pos,
+        },
         SpecExpr::Field { field, x, pos } => SpecExpr::Field {
             field,
             x: Box::new(substitute(*x, substitutions)?),

cranelift/isle/veri/veri/filetests/pass/type_qualifier.isle

@@ -0,0 +1,25 @@
+; Test case that requires type qualifier to satisfy type inference.
+
+; Value type of unspecified bit-vector width.
+(type Value (primitive Value))
+(model Value (type (bv)))
+
+; Top-level test term asserts equality
+(decl test (Value) Value)
+(spec (test arg) (provide (= result arg)))
+
+; Add then mask low byte.
+;
+; Note the (as ...) type qualifier. Without it, this test case would have
+; underconstrained type inference.
+(decl add_then_mask (Value Value) Value)
+(extern extractor add_then_mask add_then_mask)
+(spec (add_then_mask x y) (match (= result (extract 7 0 (bvadd x (as y (bv 16)))))))
+
+; Mask low byte then add.
+(decl mask_then_add (Value Value) Value)
+(extern constructor mask_then_add mask_then_add)
+(spec (mask_then_add x y) (provide (= result (bvadd (extract 7 0 x) (extract 7 0 y)))))
+
+; Test rule swaps mask order.
+(rule test (test (add_then_mask x y)) (mask_then_add x y))

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

@@ -45,6 +45,7 @@ pub enum ExprKind {
     // Terminal nodes
     Var(Ident),
     Const(Const),
+    As(Expr, Compound),
     Constructor(Constructor),
     Field(Ident, Expr),
     Discriminator(Ident, Expr),
@@ -213,6 +214,9 @@ impl ExprKind {
                 ExprKind::Const(Const::BitVector(*width, *val))
             }
             ast::SpecExpr::Var { var, pos: _ } => ExprKind::Var(var.clone()),
+            ast::SpecExpr::As { x, ty, pos: _ } => {
+                ExprKind::As(expr_from_ast(x), Compound::from_ast(ty))
+            }
             ast::SpecExpr::Field { field, x, pos: _ } => {
                 ExprKind::Field(field.clone(), expr_from_ast(x))
             }

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

@@ -11,7 +11,7 @@ use cranelift_isle::sema::TermId;
 use crate::{
     spec::Signature,
     types::{Compound, Const, Type, Width},
-    veri::{Call, Conditions, Expr, ExprId, Symbolic},
+    veri::{Call, Conditions, Expr, ExprId, Qualifier, Symbolic},
 };
 
 #[derive(Clone, Debug, Eq, PartialEq)]
@@ -260,6 +260,11 @@ impl<'a> SystemBuilder<'a> {
             self.call(call);
         }
 
+        // Qualifiers.
+        for qualifier in &self.conditions.qualifiers {
+            self.qualifier(qualifier);
+        }
+
         self.system
     }
 
@@ -451,6 +456,10 @@ impl<'a> SystemBuilder<'a> {
         }
     }
 
+    fn qualifier(&mut self, qualifier: &Qualifier) {
+        self.symbolic(&qualifier.value, qualifier.ty.clone());
+    }
+
     fn symbolic(&mut self, v: &Symbolic, ty: Compound) {
         match (v, ty) {
             (Symbolic::Scalar(x), Compound::Primitive(ty)) => self.ty(*x, ty),

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

@@ -601,6 +601,13 @@ pub struct Call {
     pub signatures: Vec<Signature>,
 }
 
+// Type qualifier, for example derived from an `(as ...)` expression.
+#[derive(Debug)]
+pub struct Qualifier {
+    pub value: Symbolic,
+    pub ty: Compound,
+}
+
 /// Verification conditions for an expansion.
 #[derive(Debug, Default)]
 pub struct Conditions {
@@ -609,6 +616,7 @@ pub struct Conditions {
     pub assertions: Vec<ExprId>,
     pub variables: Vec<Variable>,
     pub calls: Vec<Call>,
+    pub qualifiers: Vec<Qualifier>,
 }
 
 impl Conditions {
@@ -1614,6 +1622,15 @@ impl<'a> ConditionsBuilder<'a> {
                 let x = self.spec_expr(x, vars)?.try_into()?;
                 Ok(self.scalar(Expr::WidthOf(x)))
             }
+
+            spec::ExprKind::As(x, ty) => {
+                let x = self.spec_expr(x, vars)?;
+                self.conditions.qualifiers.push(Qualifier {
+                    value: x.clone(),
+                    ty: ty.clone(),
+                });
+                Ok(x)
+            }
         }
     }