Update OCaml

Author: N1ark

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.165"
+let supported_charon_version = "0.1.166"

charon-ml/src/PrintGAst.ml

@@ -28,11 +28,16 @@ let call_to_string (env : 'a fmt_env) (indent : string) (call : call) : string =
   let dest = place_to_string env call.dest in
   indent ^ dest ^ " := move " ^ func ^ args
 
-let assertion_to_string (env : 'a fmt_env) (indent : string) (a : assertion) :
-    string =
+let assertion_to_string (env : 'a fmt_env) (a : assertion) : string =
   let cond = operand_to_string env a.cond in
-  if a.expected then indent ^ "assert(" ^ cond ^ ")"
-  else indent ^ "assert(¬" ^ cond ^ ")"
+  if a.expected then "assert(" ^ cond ^ ")" else "assert(¬" ^ cond ^ ")"
+
+let abort_kind_to_string (env : 'a fmt_env) (a : abort_kind) : string =
+  match a with
+  | Panic None -> "panic"
+  | Panic (Some name) -> "panic(" ^ name_to_string env name ^ ")"
+  | UndefinedBehavior -> "undefined_behavior"
+  | UnwindTerminate -> "unwind_terminate"
 
 (** Small helper *)
 let fun_sig_with_name_to_string (env : 'a fmt_env) (indent : string)

charon-ml/src/PrintLlbcAst.ml

@@ -37,7 +37,11 @@ module Ast = struct
         indent ^ "storage_dead " ^ local_id_to_string env var_id
     | Deinit p -> indent ^ "deinit " ^ place_to_string env p
     | Drop (p, _, _) -> indent ^ "drop " ^ place_to_string env p
-    | Assert a -> assertion_to_string env indent a
+    | Assert (asrt, abort_kind) ->
+        indent
+        ^ assertion_to_string env asrt
+        ^ " else "
+        ^ abort_kind_to_string env abort_kind
     | Call call -> call_to_string env indent call
     | Abort (Panic _) -> indent ^ "panic"
     | Abort UndefinedBehavior -> indent ^ "undefined_behavior"

charon-ml/src/PrintUllbcAst.ml

@@ -27,7 +27,11 @@ module Ast = struct
         indent ^ "set_discriminant(" ^ place_to_string env p ^ ", "
         ^ variant_id_to_pretty_string variant_id
         ^ ")"
-    | Assert a -> assertion_to_string env indent a
+    | Assert (asrt, abort_kind) ->
+        indent
+        ^ assertion_to_string env asrt
+        ^ " else "
+        ^ abort_kind_to_string env abort_kind
     | StorageLive var_id ->
         indent ^ "storage_live " ^ local_id_to_string env var_id
     | StorageDead var_id ->
@@ -75,6 +79,11 @@ module Ast = struct
     | Drop (_, p, _, tgt, unwind) ->
         indent ^ "drop " ^ place_to_string env p ^ " -> "
         ^ block_id_to_string tgt ^ "(unwind:" ^ block_id_to_string unwind ^ ")"
+    | TAssert (asrt, tgt, unwind) ->
+        indent
+        ^ assertion_to_string env asrt
+        ^ " -> " ^ block_id_to_string tgt ^ "(unwind:"
+        ^ block_id_to_string unwind ^ ")"
     | Abort _ -> indent ^ "panic"
     | Return -> indent ^ "return"
     | UnwindResume -> indent ^ "unwind_continue"

charon-ml/src/generated/Generated_GAst.ml

@@ -23,14 +23,17 @@ type fn_ptr_kind = Types.fn_ptr_kind [@@deriving show, ord]
 type fun_decl_id = Types.fun_decl_id [@@deriving show, ord]
 
 (** (U)LLBC is a language with side-effects: a statement may abort in a way that
-    isn't tracked by control-flow. The two kinds of abort are:
-    - Panic (may unwind or not depending on compilation setting);
-    - Undefined behavior: *)
+    isn't tracked by control-flow. The three kinds of abort are:
+    - Panic
+    - Undefined behavior (caused by an "assume")
+    - Unwind termination *)
 type abort_kind =
-  | Panic of name option  (** A built-in panicking function. *)
+  | Panic of name option
+      (** A built-in panicking function, or a panic due to a failed built-in
+          check (e.g. for out-of-bounds accesses). *)
   | UndefinedBehavior  (** Undefined behavior in the rust abstract machine. *)
   | UnwindTerminate
-      (** Unwind had to stop for Abi reasons or because cleanup code panicked
+      (** Unwind had to stop for ABI reasons or because cleanup code panicked
           again. *)
 
 (** Check the value of an operand and abort if the value is not expected. This
@@ -47,9 +50,33 @@ and assertion = {
   expected : bool;
       (** The value that the operand should evaluate to for the assert to
           succeed. *)
-  on_failure : abort_kind;  (** What kind of abort happens on assert failure. *)
+  check_kind : builtin_assert_kind option;
+      (** The kind of check performed by this assert. This is only used for
+          error reporting, as the check is actually performed by the
+          instructions preceding the assert. *)
 }
 
+(** The kind of a built-in assertion, which may panic and unwind. These are
+    removed by [reconstruct_fallible_operations] because they're implicit in the
+    semantics of (U)LLBC. This kind should only be used for error-reporting
+    purposes, as the check itself is performed in the instructions preceding the
+    assert. *)
+and builtin_assert_kind =
+  | BoundsCheck of operand * operand
+      (** Fields:
+          - [len]
+          - [index] *)
+  | Overflow of binop * operand * operand
+  | OverflowNeg of operand
+  | DivisionByZero of operand
+  | RemainderByZero of operand
+  | MisalignedPointerDereference of operand * operand
+      (** Fields:
+          - [required]
+          - [found] *)
+  | NullPointerDereference
+  | InvalidEnumConstruction of operand
+
 and call = { func : fn_operand; args : operand list; dest : place }
 and copy_non_overlapping = { src : operand; dst : operand; count : operand }
 

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -117,12 +117,14 @@ and assertion_of_json (ctx : of_json_ctx) (js : json) :
   combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc
-        [ ("cond", cond); ("expected", expected); ("on_failure", on_failure) ]
+        [ ("cond", cond); ("expected", expected); ("check_kind", check_kind) ]
       ->
         let* cond = operand_of_json ctx cond in
         let* expected = bool_of_json ctx expected in
-        let* on_failure = abort_kind_of_json ctx on_failure in
-        Ok ({ cond; expected; on_failure } : assertion)
+        let* check_kind =
+          option_of_json builtin_assert_kind_of_json ctx check_kind
+        in
+        Ok ({ cond; expected; check_kind } : assertion)
     | _ -> Error "")
 
 and attr_info_of_json (ctx : of_json_ctx) (js : json) :
@@ -250,6 +252,44 @@ and borrow_kind_of_json (ctx : of_json_ctx) (js : json) :
     | `String "UniqueImmutable" -> Ok BUniqueImmutable
     | _ -> Error "")
 
+and builtin_assert_kind_of_json (ctx : of_json_ctx) (js : json) :
+    (builtin_assert_kind, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("BoundsCheck", `Assoc [ ("len", len); ("index", index) ]) ] ->
+        let* len = operand_of_json ctx len in
+        let* index = operand_of_json ctx index in
+        Ok (BoundsCheck (len, index))
+    | `Assoc [ ("Overflow", `List [ x_0; x_1; x_2 ]) ] ->
+        let* x_0 = binop_of_json ctx x_0 in
+        let* x_1 = operand_of_json ctx x_1 in
+        let* x_2 = operand_of_json ctx x_2 in
+        Ok (Overflow (x_0, x_1, x_2))
+    | `Assoc [ ("OverflowNeg", overflow_neg) ] ->
+        let* overflow_neg = operand_of_json ctx overflow_neg in
+        Ok (OverflowNeg overflow_neg)
+    | `Assoc [ ("DivisionByZero", division_by_zero) ] ->
+        let* division_by_zero = operand_of_json ctx division_by_zero in
+        Ok (DivisionByZero division_by_zero)
+    | `Assoc [ ("RemainderByZero", remainder_by_zero) ] ->
+        let* remainder_by_zero = operand_of_json ctx remainder_by_zero in
+        Ok (RemainderByZero remainder_by_zero)
+    | `Assoc
+        [
+          ( "MisalignedPointerDereference",
+            `Assoc [ ("required", required); ("found", found) ] );
+        ] ->
+        let* required = operand_of_json ctx required in
+        let* found = operand_of_json ctx found in
+        Ok (MisalignedPointerDereference (required, found))
+    | `String "NullPointerDereference" -> Ok NullPointerDereference
+    | `Assoc [ ("InvalidEnumConstruction", invalid_enum_construction) ] ->
+        let* invalid_enum_construction =
+          operand_of_json ctx invalid_enum_construction
+        in
+        Ok (InvalidEnumConstruction invalid_enum_construction)
+    | _ -> Error "")
+
 and builtin_fun_id_of_json (ctx : of_json_ctx) (js : json) :
     (builtin_fun_id, string) result =
   combine_error_msgs js __FUNCTION__

charon-ml/src/generated/Generated_LlbcAst.ml

@@ -50,7 +50,10 @@ and statement_kind =
           or a conditional call that should only happen if the place has not
           been moved out of. See the docs of [DropKind] for more details; to get
           precise drops use [--precise-drops]. *)
-  | Assert of assertion
+  | Assert of assertion * abort_kind
+      (** Fields:
+          - [assert]
+          - [on_failure] *)
   | Call of call
   | Abort of abort_kind
       (** Panic also handles "unreachable". We keep the name of the panicking

charon-ml/src/generated/Generated_LlbcOfJson.ml

@@ -72,9 +72,13 @@ and statement_kind_of_json (ctx : of_json_ctx) (js : json) :
         let* x_1 = trait_ref_of_json ctx x_1 in
         let* x_2 = drop_kind_of_json ctx x_2 in
         Ok (Drop (x_0, x_1, x_2))
-    | `Assoc [ ("Assert", assert_) ] ->
+    | `Assoc
+        [
+          ("Assert", `Assoc [ ("assert", assert_); ("on_failure", on_failure) ]);
+        ] ->
         let* assert_ = assertion_of_json ctx assert_ in
-        Ok (Assert assert_)
+        let* on_failure = abort_kind_of_json ctx on_failure in
+        Ok (Assert (assert_, on_failure))
     | `Assoc [ ("Call", call) ] ->
         let* call = call_of_json ctx call in
         Ok (Call call)

charon-ml/src/generated/Generated_UllbcAst.ml

@@ -35,12 +35,16 @@ and statement_kind =
           the function's body, in which case it is implicitly deallocated at the
           end of the function. *)
   | Deinit of place
-  | Assert of assertion
-      (** A runtime check for a condition. This can be either:
-          - Emitted for bounds/overflow/etc checks if
-            [--reconstruct-fallible-operations] is not set;
-          - Reconstructed from [if b { panic() }] if [--reconstruct-assets] is
-            set. *)
+  | Assert of assertion * abort_kind
+      (** A non-diverging runtime check for a condition. This can be either:
+          - Emitted for inlined "assumes" (which cause UB on failure)
+          - Reconstructed from [if b { panic() }] if [--reconstruct-asserts] is
+            set. This statement comes with the effect that happens when the
+            check fails (rather than representing it as an unwinding edge).
+
+          Fields:
+          - [assert]
+          - [on_failure] *)
   | Nop  (** Does nothing. Useful for passes. *)
 
 and switch =
@@ -107,6 +111,14 @@ and terminator_kind =
           - [tref]
           - [target]
           - [on_unwind] *)
+  | TAssert of assertion * block_id * block_id
+      (** Assert that the given condition holds, and if not, unwind to the given
+          block. This is used for bounds checks, overflow checks, etc.
+
+          Fields:
+          - [assert]
+          - [target]
+          - [on_unwind] *)
   | Abort of abort_kind  (** Handles panics and impossible cases. *)
   | Return
   | UnwindResume

charon-ml/src/generated/Generated_UllbcOfJson.ml

@@ -63,9 +63,13 @@ and statement_kind_of_json (ctx : of_json_ctx) (js : json) :
     | `Assoc [ ("Deinit", deinit) ] ->
         let* deinit = place_of_json ctx deinit in
         Ok (Deinit deinit)
-    | `Assoc [ ("Assert", assert_) ] ->
+    | `Assoc
+        [
+          ("Assert", `Assoc [ ("assert", assert_); ("on_failure", on_failure) ]);
+        ] ->
         let* assert_ = assertion_of_json ctx assert_ in
-        Ok (Assert assert_)
+        let* on_failure = abort_kind_of_json ctx on_failure in
+        Ok (Assert (assert_, on_failure))
     | `String "Nop" -> Ok Nop
     | _ -> Error "")
 
@@ -141,6 +145,18 @@ and terminator_kind_of_json (ctx : of_json_ctx) (js : json) :
         let* target = block_id_of_json ctx target in
         let* on_unwind = block_id_of_json ctx on_unwind in
         Ok (Drop (kind, place, tref, target, on_unwind))
+    | `Assoc
+        [
+          ( "Assert",
+            `Assoc
+              [
+                ("assert", assert_); ("target", target); ("on_unwind", on_unwind);
+              ] );
+        ] ->
+        let* assert_ = assertion_of_json ctx assert_ in
+        let* target = block_id_of_json ctx target in
+        let* on_unwind = block_id_of_json ctx on_unwind in
+        Ok (TAssert (assert_, target, on_unwind))
     | `Assoc [ ("Abort", abort) ] ->
         let* abort = abort_kind_of_json ctx abort in
         Ok (Abort abort)