Implemented __VERIFIER_assume hook (rust-lang#115)

Author: danielsn

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs

@@ -187,7 +187,7 @@ impl Stmt {
 
     /// `__CPROVER_assume(cond);`
     pub fn assume(cond: Expr, loc: Location) -> Self {
-        assert!(cond.typ().is_bool());
+        assert!(cond.typ().is_bool(), "Assume expected bool, got {:?}", cond);
         stmt!(Assume { cond }, loc)
     }
 

compiler/rustc_codegen_llvm/src/gotoc/hooks.rs

@@ -48,6 +48,40 @@ fn sig_of_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> ty::FnS
     tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig)
 }
 
+struct Assume;
+impl<'tcx> GotocHook<'tcx> for Assume {
+    fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
+        let sig = sig_of_instance(tcx, instance);
+        let def_path = tcx.def_path(instance.def.def_id());
+        if let Some(data) = def_path.data.last() {
+            match data.data.name() {
+                DefPathDataName::Named(name) => {
+                    return name.to_string().starts_with("__VERIFIER_assume");
+                }
+                DefPathDataName::Anon { .. } => (),
+            }
+        }
+        false
+    }
+
+    fn handle(
+        &self,
+        tcx: &mut GotocCtx<'tcx>,
+        _instance: Instance<'tcx>,
+        mut fargs: Vec<Expr>,
+        _assign_to: Option<Place<'tcx>>,
+        target: Option<BasicBlock>,
+        span: Option<Span>,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 1);
+        let cond = fargs.remove(0).cast_to(Type::bool());
+        let target = target.unwrap();
+        let loc = tcx.codegen_span_option2(span);
+
+        Stmt::block(vec![Stmt::assume(cond, loc.clone()), Stmt::goto(tcx.find_label(&target), loc)])
+    }
+}
+
 struct Nondet;
 
 impl<'tcx> GotocHook<'tcx> for Nondet {
@@ -553,6 +587,7 @@ pub fn type_and_fn_hooks<'tcx>() -> (GotocTypeHooks<'tcx>, GotocHooks<'tcx>) {
         hooks: vec![
             Rc::new(Panic), //Must go first, so it overrides Nevers
             Rc::new(Nevers),
+            Rc::new(Assume),
             Rc::new(Nondet),
             Rc::new(MemReplace),
             Rc::new(MemSwap),

rust-tests/cbmc-reg/Assume/main.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn __VERIFIER_assume(cond: bool) {
+    unimplemented!()
+}
+
+fn __nondet<T>() -> T {
+    unimplemented!()
+}
+
+fn main() {
+    let i: i32 = __nondet();
+    __VERIFIER_assume(i < 10);
+    assert!(i < 20);
+}

rust-tests/cbmc-reg/Assume/main_fail.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn __VERIFIER_assume(cond: bool) {
+    unimplemented!()
+}
+
+fn __nondet<T>() -> T {
+    unimplemented!()
+}
+
+fn main() {
+    let i: i32 = __nondet();
+    __VERIFIER_assume(i < 10);
+    assert!(i > 20);
+}