veri: implies spec op (#99)

This PR implements the implies => spec operator.

Note this operator already exists in the annotation IR and veri IR levels, so
this PR just does the plumbing to connect up to the parser.

cranelift/codegen/src/isa/aarch64/lower/isle.rs

@@ -22,8 +22,8 @@ use crate::machinst::{isle::*, InputSourceInst};
 use crate::{
     binemit::CodeOffset,
     ir::{
-        immediates::*, types::*, AtomicRmwOp, BlockCall, ExternalName, Inst, InstructionData,
-        MemFlags, TrapCode, Value, ValueList,
+        immediates::*, types::*, ArgumentExtension, AtomicRmwOp, BlockCall, ExternalName, Inst,
+        InstructionData, MemFlags, TrapCode, Value, ValueList,
     },
     isa::aarch64::abi::AArch64CallSite,
     isa::aarch64::inst::args::{ShiftOp, ShiftOpShiftImm},

cranelift/isle/isle/isle_examples/pass/veri_spec.isle

@@ -8,7 +8,7 @@
   ((args (bv 64)) (ret (bv 64)) (canon (bv 64)))
 )
 
-(spec (A i j) (provide (= (if true (= i j) (= i (bvneg j))))))
+(spec (A i j) (provide (= (if true (= i j) (= i (bvneg j))) (=> false true))))
 (instantiate A ((args (bv 8)) (ret (bv 8)) (canon (bv 8))))
 (decl A (u8 u8) u8)
 

cranelift/isle/isle/src/ast.rs

@@ -141,6 +141,7 @@ pub enum SpecOp {
     And,
     Or,
     Not,
+    Imp,
 
     // Integer comparisons
     Lt,

cranelift/isle/isle/src/parser.rs

@@ -474,6 +474,7 @@ impl<'a> Parser<'a> {
             "=" => Ok(SpecOp::Eq),
             "and" => Ok(SpecOp::And),
             "not" => Ok(SpecOp::Not),
+            "=>" => Ok(SpecOp::Imp),
             "or" => Ok(SpecOp::Or),
             "<=" => Ok(SpecOp::Lte),
             "<" => Ok(SpecOp::Lt),

cranelift/isle/isle/src/printer.rs

@@ -228,6 +228,7 @@ impl Printable for SpecOp {
             SpecOp::Eq => "=",
             SpecOp::And => "and",
             SpecOp::Not => "not",
+            SpecOp::Imp => "=>",
             SpecOp::Or => "or",
             SpecOp::Lte => "<=",
             SpecOp::Lt => "<",

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

@@ -141,6 +141,7 @@ fn spec_op_to_expr(s: &SpecOp, args: &Vec<SpecExpr>, pos: &Pos, env: &ParsingEnv
         SpecOp::Lte => binop(|x, y| Expr::Lte(x, y), args, pos, env),
         SpecOp::Gt => binop(|x, y| Expr::Lt(y, x), args, pos, env),
         SpecOp::Gte => binop(|x, y| Expr::Lte(y, x), args, pos, env),
+        SpecOp::Imp => binop(|x, y| Expr::Imp(x, y), args, pos, env),
         SpecOp::BVAnd => binop(|x, y| Expr::BVAnd(x, y), args, pos, env),
         SpecOp::BVOr => binop(|x, y| Expr::BVOr(x, y), args, pos, env),
         SpecOp::BVXor => binop(|x, y| Expr::BVXor(x, y), args, pos, env),

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

@@ -446,6 +446,24 @@ fn add_annotation_constraints(
                 t,
             )
         }
+        annotation_ir::Expr::Imp(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(t1, annotation_ir::Type::Bool));
+            tree.concrete_constraints
+                .insert(TypeExpr::Concrete(t2, annotation_ir::Type::Bool));
+            tree.concrete_constraints
+                .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
+
+            tree.next_type_var += 1;
+            (
+                veri_ir::Expr::Binary(veri_ir::BinaryOp::Imp, Box::new(e1), Box::new(e2)),
+                t,
+            )
+        }
         annotation_ir::Expr::Lte(x, y) => {
             let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
             let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
@@ -1358,8 +1376,6 @@ fn add_annotation_constraints(
             tree.next_type_var += 1;
             (veri_ir::Expr::BVPopcnt(Box::new(e1)), t)
         }
-
-        _ => todo!("expr {:#?} not yet implemented", expr),
     };
     tree.ty_vars.insert(e.clone(), t);
     // let fmt = format!("{}:\t{:?}", t, e);