Support assume intrinsic

charon-ml/src/PrintUllbcAst.ml

@@ -31,6 +31,7 @@ module Ast = struct
     | StorageDead var_id ->
         indent ^ "storage_dead " ^ var_id_to_string env var_id
     | Deinit p -> indent ^ "deinit " ^ place_to_string env p
+    | StAssert a -> assertion_to_string env indent a
 
   let switch_to_string (indent : string) (tgt : switch) : string =
     match tgt with

charon-ml/src/UllbcAst.ml

@@ -36,6 +36,7 @@ and raw_statement =
       (** We translate this to [crate::llbc_ast::RawStatement::Drop] in LLBC *)
   | Deinit of place
       (** We translate this to [crate::llbc_ast::RawStatement::Drop] in LLBC *)
+  | StAssert of assertion
 [@@deriving
   show,
     visitors

charon-ml/src/UllbcOfJson.ml

@@ -43,6 +43,9 @@ and raw_statement_of_json (js : json) : (raw_statement, string) result =
     | `Assoc [ ("Deinit", deinit) ] ->
         let* deinit = place_of_json deinit in
         Ok (Deinit deinit)
+    | `Assoc [ ("Assert", assert_) ] ->
+        let* assert_ = assertion_of_json assert_ in
+        Ok (StAssert assert_)
     | _ -> Error "")
 
 and switch_of_json (js : json) : (switch, string) result =

charon/src/ast/ullbc_ast.rs

@@ -29,6 +29,8 @@ pub enum RawStatement {
     StorageDead(VarId),
     /// We translate this to [crate::llbc_ast::RawStatement::Drop] in LLBC
     Deinit(Place),
+    #[charon::rename("StAssert")]
+    Assert(Assert),
     #[charon::opaque]
     Error(String),
 }

charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs

@@ -942,8 +942,16 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let t_place = self.translate_place(span, place)?;
                 Some(RawStatement::Deinit(t_place))
             }
-            StatementKind::Intrinsic(_) => {
-                error_or_panic!(self, span, "Unsupported statement kind: intrinsic");
+            // This asserts the operand true on pain of UB. We treat it like a normal assertion.
+            StatementKind::Intrinsic(hax::NonDivergingIntrinsic::Assume(op)) => {
+                let op = self.translate_operand(span, op)?;
+                Some(RawStatement::Assert(Assert {
+                    cond: op,
+                    expected: true,
+                }))
+            }
+            StatementKind::Intrinsic(hax::NonDivergingIntrinsic::CopyNonOverlapping(..)) => {
+                error_or_panic!(self, span, "Unsupported statement kind: CopyNonOverlapping");
             }
             // This is for the stacked borrows memory model.
             StatementKind::Retag(_, _) => None,

charon/src/pretty/fmt_with_ctx.rs

@@ -968,6 +968,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for ullbc::Statement {
             RawStatement::Deinit(place) => {
                 format!("@deinit({})", place.fmt_with_ctx(ctx))
             }
+            RawStatement::Assert(assert) => format!("{}", assert.fmt_with_ctx(ctx)),
             RawStatement::Error(s) => {
                 format!("@Error({})", s)
             }

charon/src/transform/ullbc_to_llbc.rs

@@ -1463,6 +1463,7 @@ fn translate_statement(st: &src::Statement) -> Option<tgt::Statement> {
         src::RawStatement::StorageDead(var_id) => tgt::RawStatement::Drop(Place::new(var_id)),
         // We translate a deinit as a drop
         src::RawStatement::Deinit(place) => tgt::RawStatement::Drop(place),
+        src::RawStatement::Assert(assert) => tgt::RawStatement::Assert(assert),
         src::RawStatement::Error(s) => tgt::RawStatement::Error(s),
     };
     Some(tgt::Statement::new(src_span, st))

charon/tests/ui/issue-91-enum-to-discriminant-cast.out

@@ -1,9 +1,138 @@
-error: Unsupported statement kind: intrinsic
-  --> tests/ui/issue-91-enum-to-discriminant-cast.rs:16:13
-   |
-16 |     let _ = x as isize;
-   |             ^^^^^^^^^^
+# Final LLBC before serialization:
+
+enum test_crate::Foo =
+|  A()
+|  B()
+
+
+trait core::clone::Clone<Self>
+{
+    fn clone : core::clone::Clone::clone
+    fn clone_from : core::clone::Clone::clone_from
+}
+
+trait core::marker::Copy<Self>
+{
+    parent_clause_0 : [@TraitClause0]: core::clone::Clone<Self>
+}
+
+fn test_crate::{impl core::clone::Clone for test_crate::Foo}#1::clone<'_0>(@1: &'_0 (test_crate::Foo)) -> test_crate::Foo
+{
+    let @0: test_crate::Foo; // return
+    let self@1: &'_ (test_crate::Foo); // arg #1
+
+    @0 := copy (*(self@1))
+    return
+}
+
+impl test_crate::{impl core::clone::Clone for test_crate::Foo}#1 : core::clone::Clone<test_crate::Foo>
+{
+    fn clone = test_crate::{impl core::clone::Clone for test_crate::Foo}#1::clone
+}
+
+impl test_crate::{impl core::marker::Copy for test_crate::Foo} : core::marker::Copy<test_crate::Foo>
+{
+    parent_clause0 = test_crate::{impl core::clone::Clone for test_crate::Foo}#1
+}
+
+enum test_crate::Ordering =
+|  Less()
+|  Equal()
+|  Greater()
+
+
+fn test_crate::main()
+{
+    let @0: (); // return
+    let x@1: test_crate::Foo; // local
+    let @2: isize; // anonymous local
+    let @3: test_crate::Foo; // anonymous local
+    let @4: isize; // anonymous local
+    let @5: u8; // anonymous local
+    let @6: bool; // anonymous local
+    let @7: u8; // anonymous local
+    let @8: test_crate::Foo; // anonymous local
+    let @9: isize; // anonymous local
+    let @10: u8; // anonymous local
+    let @11: bool; // anonymous local
+    let x@12: test_crate::Ordering; // local
+    let @13: isize; // anonymous local
+    let @14: test_crate::Ordering; // anonymous local
+    let @15: isize; // anonymous local
+    let @16: u8; // anonymous local
+    let @17: bool; // anonymous local
+    let @18: bool; // anonymous local
+    let @19: bool; // anonymous local
+    let @20: (); // anonymous local
+
+    x@1 := test_crate::Foo::A {  }
+    @fake_read(x@1)
+    @3 := copy (x@1)
+    match @3 {
+        0 => {
+            @4 := const (0 : isize)
+        },
+        1 => {
+            @4 := const (1 : isize)
+        }
+    }
+    @5 := cast<isize, u8>(copy (@4))
+    @6 := copy (@5) <= const (1 : u8)
+    assert(move (@6) == true)
+    @2 := cast<isize, isize>(move (@4))
+    drop @3
+    @fake_read(@2)
+    drop @2
+    @8 := copy (x@1)
+    match @8 {
+        0 => {
+            @9 := const (0 : isize)
+        },
+        1 => {
+            @9 := const (1 : isize)
+        }
+    }
+    @10 := cast<isize, u8>(copy (@9))
+    @11 := copy (@10) <= const (1 : u8)
+    assert(move (@11) == true)
+    @7 := cast<isize, u8>(move (@9))
+    drop @8
+    @fake_read(@7)
+    drop @7
+    x@12 := test_crate::Ordering::Greater {  }
+    @fake_read(x@12)
+    @14 := move (x@12)
+    match @14 {
+        0 => {
+            @15 := const (-1 : isize)
+        },
+        1 => {
+            @15 := const (0 : isize)
+        },
+        2 => {
+            @15 := const (1 : isize)
+        }
+    }
+    @16 := cast<isize, u8>(copy (@15))
+    @17 := copy (@16) >= const (255 : u8)
+    @18 := copy (@16) <= const (1 : u8)
+    @19 := move (@17) | move (@18)
+    assert(move (@19) == true)
+    @13 := cast<isize, isize>(move (@15))
+    drop @14
+    @fake_read(@13)
+    drop @13
+    @20 := ()
+    @0 := move (@20)
+    drop x@12
+    drop x@1
+    @0 := ()
+    return
+}
+
+fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
+
+fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self))
+
 
-error: aborting due to 1 previous error
 
-Error: Charon driver exited with code 101

charon/tests/ui/issue-91-enum-to-discriminant-cast.rs

@@ -1,4 +1,3 @@
-//@ known-failure
 #[derive(Copy, Clone)]
 enum Foo {
     A,

charon/tests/ui/unsafe.out

@@ -100,5 +100,16 @@ fn test_crate::access_union_field()
     return
 }
 
+unsafe fn core::intrinsics::assume(@1: bool)
+
+fn test_crate::assume()
+{
+    let @0: (); // return
+
+    @0 := core::intrinsics::assume(const (true))
+    @0 := ()
+    return
+}
+
 
 

charon/tests/ui/unsafe.rs

@@ -34,3 +34,7 @@ fn access_union_field() {
     let one = Foo { one: 42 };
     let _two = unsafe { one.two };
 }
+
+fn assume() {
+    std::intrinsics::assume(true)
+}