Merge linear control-flow before reconstruction

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.37"
+let supported_charon_version = "0.1.38"

charon-ml/src/PrintUllbcAst.ml

@@ -31,7 +31,9 @@ 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
+    | Assert a -> assertion_to_string env indent a
+    | Drop p -> indent ^ "drop " ^ place_to_string env p
+    | Call call -> call_to_string env indent call
 
   let switch_to_string (indent : string) (tgt : switch) : string =
     match tgt with
@@ -63,16 +65,6 @@ module Ast = struct
         ^ switch_to_string indent tgts
     | Abort _ -> indent ^ "panic"
     | Return -> indent ^ "return"
-    | Drop (p, bid) ->
-        indent ^ "drop " ^ place_to_string env p ^ ";\n" ^ indent ^ "goto "
-        ^ block_id_to_string bid
-    | Call (call, bid) -> (
-        call_to_string env indent call
-        ^ ";\n" ^ indent ^ "goto "
-        ^ match bid with Some bid -> block_id_to_string bid | None -> "!")
-    | Assert (a, bid) ->
-        assertion_to_string env indent a
-        ^ ";\n" ^ indent ^ "goto " ^ block_id_to_string bid
 
   let block_to_string (env : fmt_env) (indent : string) (indent_incr : string)
       (id : BlockId.id) (block : block) : string =

charon-ml/src/UllbcAst.ml

@@ -30,13 +30,19 @@ type statement = { span : span; content : raw_statement }
 (** A raw statement: a statement without meta data. *)
 and raw_statement =
   | Assign of place * rvalue
+  | Call of call
+      (** A call. For now, we don't support dynamic calls (i.e. to a function pointer in memory). *)
   | FakeRead of place
   | SetDiscriminant of place * variant_id
   | StorageDead of var_id
       (** 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
+  | Drop of place
+  | Assert of assertion
+      (** A built-in assert, which corresponds to runtime checks that we remove, namely: bounds
+          checks, over/underflow checks, div/rem by zero checks, pointer alignement check.
+       *)
 [@@deriving
   show,
     visitors
@@ -98,28 +104,6 @@ and raw_terminator =
        *)
   | Abort of abort_kind  (** Handles panics and impossible cases. *)
   | Return
-  | Drop of place * block_id
-      (** 
-          Fields:
-          - [place]
-          - [target]
-       *)
-  | Call of call * block_id option
-      (** Function call. If `target` is `None`, the function is guaranteed to diverge.
-          For now, we don't support dynamic calls (i.e. to a function pointer in memory).
-
-          Fields:
-          - [call]
-          - [target]
-       *)
-  | Assert of assertion * block_id
-      (** A built-in assert, which corresponds to runtime checks that we remove, namely: bounds
-          checks, over/underflow checks, div/rem by zero checks, pointer alignement check.
-
-          Fields:
-          - [assert]
-          - [target]
-       *)
 [@@deriving
   show,
     visitors

charon-ml/src/UllbcOfJson.ml

@@ -30,6 +30,9 @@ and raw_statement_of_json (js : json) : (raw_statement, string) result =
         let* x_0 = place_of_json x_0 in
         let* x_1 = rvalue_of_json x_1 in
         Ok (Assign (x_0, x_1))
+    | `Assoc [ ("Call", call) ] ->
+        let* call = call_of_json call in
+        Ok (Call call)
     | `Assoc [ ("FakeRead", fake_read) ] ->
         let* fake_read = place_of_json fake_read in
         Ok (FakeRead fake_read)
@@ -43,9 +46,12 @@ 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 [ ("Drop", drop) ] ->
+        let* drop = place_of_json drop in
+        Ok (Drop drop)
     | `Assoc [ ("Assert", assert_) ] ->
         let* assert_ = assertion_of_json assert_ in
-        Ok (StAssert assert_)
+        Ok (Assert assert_)
     | _ -> Error "")
 
 and switch_of_json (js : json) : (switch, string) result =
@@ -90,19 +96,6 @@ and raw_terminator_of_json (id_to_file : id_to_file_map) (js : json) :
         let* abort = abort_kind_of_json id_to_file abort in
         Ok (Abort abort)
     | `String "Return" -> Ok Return
-    | `Assoc [ ("Drop", `Assoc [ ("place", place); ("target", target) ]) ] ->
-        let* place = place_of_json place in
-        let* target = block_id_of_json target in
-        Ok (Drop (place, target))
-    | `Assoc [ ("Call", `Assoc [ ("call", call); ("target", target) ]) ] ->
-        let* call = call_of_json call in
-        let* target = option_of_json block_id_of_json target in
-        Ok (Call (call, target))
-    | `Assoc [ ("Assert", `Assoc [ ("assert", assert_); ("target", target) ]) ]
-      ->
-        let* assert_ = assertion_of_json assert_ in
-        let* target = block_id_of_json target in
-        Ok (Assert (assert_, target))
     | _ -> Error "")
 
 and block_of_json (id_to_file : id_to_file_map) (js : json) :

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.37"
+version = "0.1.38"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"

charon/Makefile

@@ -3,7 +3,7 @@ all: build
 
 .PHONY: build
 build: format
-	cargo build --release
+	CARGO_PROFILE_RELEASE_DEBUG=true cargo build --release
 
 .PHONY: format
 format:

charon/src/ast/ullbc_ast.rs

@@ -23,13 +23,17 @@ pub type ExprBody = GExprBody<BodyContents>;
 )]
 pub enum RawStatement {
     Assign(Place, Rvalue),
+    /// A call. For now, we don't support dynamic calls (i.e. to a function pointer in memory).
+    Call(Call),
     FakeRead(Place),
     SetDiscriminant(Place, VariantId),
     /// We translate this to [crate::llbc_ast::RawStatement::Drop] in LLBC
     StorageDead(VarId),
     /// We translate this to [crate::llbc_ast::RawStatement::Drop] in LLBC
     Deinit(Place),
-    #[charon::rename("StAssert")]
+    Drop(Place),
+    /// A built-in assert, which corresponds to runtime checks that we remove, namely: bounds
+    /// checks, over/underflow checks, div/rem by zero checks, pointer alignement check.
     Assert(Assert),
     #[charon::opaque]
     Error(String),
@@ -76,22 +80,6 @@ pub enum RawTerminator {
     /// Handles panics and impossible cases.
     Abort(AbortKind),
     Return,
-    Drop {
-        place: Place,
-        target: BlockId,
-    },
-    /// Function call. If `target` is `None`, the function is guaranteed to diverge.
-    /// For now, we don't support dynamic calls (i.e. to a function pointer in memory).
-    Call {
-        call: Call,
-        target: Option<BlockId>,
-    },
-    /// A built-in assert, which corresponds to runtime checks that we remove, namely: bounds
-    /// checks, over/underflow checks, div/rem by zero checks, pointer alignement check.
-    Assert {
-        assert: Assert,
-        target: BlockId,
-    },
 }
 
 #[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]

charon/src/ast/ullbc_ast_utils.rs

@@ -36,6 +36,18 @@ impl Terminator {
 }
 
 impl BlockData {
+    pub fn targets(&self) -> Vec<BlockId> {
+        match &self.terminator.content {
+            RawTerminator::Goto { target } => {
+                vec![*target]
+            }
+            RawTerminator::Switch { targets, .. } => targets.get_targets(),
+            RawTerminator::Abort(..) | RawTerminator::Return => {
+                vec![]
+            }
+        }
+    }
+
     /// See [body_transform_operands]
     pub fn transform_operands<F: FnMut(&Span, &mut Vec<Statement>, &mut Operand)>(
         mut self,

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

@@ -253,7 +253,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
         // Translate the terminator
         let terminator = block.terminator.as_ref().unwrap();
-        let terminator = self.translate_terminator(body, terminator)?;
+        let terminator = self.translate_terminator(body, terminator, &mut statements)?;
 
         // Insert the block in the translated blocks
         let block = BlockData {
@@ -985,6 +985,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         &mut self,
         body: &hax::MirBody<()>,
         terminator: &hax::Terminator,
+        statements: &mut Vec<Statement>,
     ) -> Result<Terminator, Error> {
         trace!("About to translate terminator (MIR) {:?}", terminator);
         let rustc_span = terminator.source_info.span.rust_span_data.unwrap().span();
@@ -1028,10 +1029,15 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 target,
                 unwind: _, // We consider that panic is an error, and don't model unwinding
                 replace: _,
-            } => RawTerminator::Drop {
-                place: self.translate_place(rustc_span, place)?,
-                target: self.translate_basic_block_id(*target),
-            },
+            } => {
+                let place = self.translate_place(rustc_span, place)?;
+                statements.push(Statement {
+                    span,
+                    content: RawStatement::Drop(place),
+                });
+                let target = self.translate_basic_block_id(*target);
+                RawTerminator::Goto { target }
+            }
             TerminatorKind::Call {
                 fun,
                 generics,
@@ -1040,10 +1046,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 target,
                 trait_refs,
                 trait_info,
-                unwind: _, // We consider that panic is an error, and don't model unwinding
+                unwind: _, // We model unwinding as an effet, we don't represent it in control flow
                 call_source: _,
                 fn_span: _,
             } => self.translate_function_call(
+                statements,
+                span,
                 rustc_span,
                 fun,
                 generics,
@@ -1058,17 +1066,18 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 expected,
                 msg: _,
                 target,
-                unwind: _, // We consider that panic is an error, and don't model unwinding
+                unwind: _, // We model unwinding as an effet, we don't represent it in control flow
             } => {
-                let cond = self.translate_operand(rustc_span, cond)?;
+                let assert = Assert {
+                    cond: self.translate_operand(rustc_span, cond)?,
+                    expected: *expected,
+                };
+                statements.push(Statement {
+                    span,
+                    content: RawStatement::Assert(assert),
+                });
                 let target = self.translate_basic_block_id(*target);
-                RawTerminator::Assert {
-                    assert: Assert {
-                        cond,
-                        expected: *expected,
-                    },
-                    target,
-                }
+                RawTerminator::Goto { target }
             }
             TerminatorKind::FalseEdge {
                 real_target,
@@ -1151,6 +1160,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     #[allow(clippy::too_many_arguments)]
     fn translate_function_call(
         &mut self,
+        statements: &mut Vec<Statement>,
+        terminator_span: Span,
         span: rustc_span::Span,
         fun: &hax::FunOperand,
         generics: &Vec<hax::GenericArg>,
@@ -1164,7 +1175,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         // There are two cases, depending on whether this is a "regular"
         // call to a top-level function identified by its id, or if we
         // are using a local function pointer (i.e., the operand is a "move").
-        match fun {
+        let lval = self.translate_place(span, destination)?;
+        let next_block = target.map(|target| self.translate_basic_block_id(target));
+        let (fn_operand, args) = match fun {
             hax::FunOperand::Id(def_id) => {
                 // Regular function call
                 let rust_id = DefId::from(def_id);
@@ -1190,24 +1203,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         // If the call is `panic!`, then the target is `None`.
                         // I don't know in which other cases it can be `None`.
                         assert!(target.is_none());
-
                         // We ignore the arguments
-                        Ok(RawTerminator::Abort(AbortKind::Panic(name)))
+                        return Ok(RawTerminator::Abort(AbortKind::Panic(name)));
                     }
                     SubstFunIdOrPanic::Fun(fid) => {
-                        let lval = self.translate_place(span, destination)?;
-                        let next_block = target.map(|target| self.translate_basic_block_id(target));
-
-                        let call = Call {
-                            func: FnOperand::Regular(fid.func),
-                            args: fid.args.unwrap(),
-                            dest: lval,
-                        };
-
-                        Ok(RawTerminator::Call {
-                            call,
-                            target: next_block,
-                        })
+                        let fn_operand = FnOperand::Regular(fid.func);
+                        let args = fid.args.unwrap();
+                        (fn_operand, args)
                     }
                 }
             }
@@ -1216,27 +1218,30 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 // The function
                 let p = self.translate_place(span, p)?;
 
-                let lval = self.translate_place(span, destination)?;
-                let next_block = target.map(|target| self.translate_basic_block_id(target));
-
                 // TODO: we may have a problem here because as we don't
                 // know which function is being called, we may not be
                 // able to filter the arguments properly... But maybe
                 // this is rather an issue for the statement which creates
                 // the function pointer, by refering to a top-level function
                 // for instance.
                 let args = self.translate_arguments(span, args)?;
-                let call = Call {
-                    func: FnOperand::Move(p),
-                    args,
-                    dest: lval,
-                };
-                Ok(RawTerminator::Call {
-                    call,
-                    target: next_block,
-                })
+                let fn_operand = FnOperand::Move(p);
+                (fn_operand, args)
             }
-        }
+        };
+        let call = Call {
+            func: fn_operand,
+            args,
+            dest: lval,
+        };
+        statements.push(Statement {
+            span: terminator_span,
+            content: RawStatement::Call(call),
+        });
+        Ok(match next_block {
+            Some(target) => RawTerminator::Goto { target },
+            None => RawTerminator::Abort(AbortKind::UndefinedBehavior),
+        })
     }
 
     /// Evaluate function arguments in a context, and return the list of computed