Update ML

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.169"
+let supported_charon_version = "0.1.170"

charon-ml/src/PrintExpressions.ml

@@ -87,9 +87,6 @@ and nullop_to_string (env : 'a fmt_env) (op : nullop) : string =
   | SizeOf -> "size_of"
   | AlignOf -> "align_of"
   | OffsetOf _ -> "offset_of(?)"
-  | UbChecks -> "ub_checks"
-  | ContractChecks -> "contract_checks"
-  | OverflowChecks -> "overflow_checks"
 
 and unop_to_string (env : 'a fmt_env) (unop : unop) : string =
   match unop with
@@ -127,11 +124,18 @@ and binop_to_string (binop : binop) : string =
   | Cmp -> "cmp"
   | Offset -> "offset"
 
+and runtime_check_to_string (check : runtime_check) : string =
+  match check with
+  | UbChecks -> "ub_checks"
+  | ContractChecks -> "contract_checks"
+  | OverflowChecks -> "overflow_checks"
+
 and operand_to_string (env : 'a fmt_env) (op : operand) : string =
   match op with
   | Copy p -> "copy " ^ place_to_string env p
   | Move p -> "move " ^ place_to_string env p
   | Constant cv -> constant_expr_to_string env cv
+  | RuntimeCheck ck -> "check " ^ runtime_check_to_string ck
 
 and aggregate_to_string (env : 'a fmt_env) (agg : aggregate_kind)
     (fields : operand list) : string =
@@ -222,6 +226,4 @@ and rvalue_to_string (env : 'a fmt_env) (rv : rvalue) : string =
       "[" ^ operand_to_string env v ^ ";"
       ^ constant_expr_to_string env len
       ^ "]"
-  | ShallowInitBox (op, _) ->
-      "shallow-init-box(" ^ operand_to_string env op ^ ")"
   | Aggregate (akind, ops) -> aggregate_to_string env akind ops

charon-ml/src/generated/Generated_Expressions.ml

@@ -167,15 +167,14 @@ and nullop =
   | SizeOf
   | AlignOf
   | OffsetOf of type_decl_ref * variant_id option * field_id
-  | UbChecks
-  | OverflowChecks
-  | ContractChecks
 
 and operand =
   | Copy of place
   | Move of place
   | Constant of constant_expr
       (** Constant value (including constant and static variables) *)
+  | RuntimeCheck of runtime_check
+      (** Whether a particular runtime check should be performed or not. *)
 
 and overflow_mode =
   | OPanic
@@ -240,6 +239,8 @@ and projection_elem =
           - [to]
           - [from_end] *)
 
+and runtime_check = UbChecks | OverflowChecks | ContractChecks
+
 (** TODO: we could factor out [Rvalue] and function calls (for LLBC, not ULLBC).
     We can also factor out the unops, binops with the function calls. TODO: move
     the aggregate kind to operands TODO: we should prefix the type variants with
@@ -310,11 +311,6 @@ and rvalue =
       (** [Repeat(x, n)] creates an array where [x] is copied [n] times.
 
           We translate this to a function call for LLBC. *)
-  | ShallowInitBox of operand * ty
-      (** Transmutes a [*mut u8] (obtained from [malloc]) into
-          shallow-initialized [Box<T>]. This only appears as part of lowering
-          [Box::new()] in some cases. We reconstruct the original [Box::new()]
-          call, but sometimes may fail to do so, leaking the expression. *)
 
 (** Unary operation *)
 and unop =

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1454,9 +1454,6 @@ and nullop_of_json (ctx : of_json_ctx) (js : json) : (nullop, string) result =
         let* x_1 = option_of_json variant_id_of_json ctx x_1 in
         let* x_2 = field_id_of_json ctx x_2 in
         Ok (OffsetOf (x_0, x_1, x_2))
-    | `String "UbChecks" -> Ok UbChecks
-    | `String "OverflowChecks" -> Ok OverflowChecks
-    | `String "ContractChecks" -> Ok ContractChecks
     | _ -> Error "")
 
 and operand_of_json (ctx : of_json_ctx) (js : json) : (operand, string) result =
@@ -1471,6 +1468,9 @@ and operand_of_json (ctx : of_json_ctx) (js : json) : (operand, string) result =
     | `Assoc [ ("Const", const) ] ->
         let* const = box_of_json constant_expr_of_json ctx const in
         Ok (Constant const)
+    | `Assoc [ ("RuntimeCheck", runtime_check) ] ->
+        let* runtime_check = runtime_check_of_json ctx runtime_check in
+        Ok (RuntimeCheck runtime_check)
     | _ -> Error "")
 
 and outlives_pred_of_json :
@@ -1700,6 +1700,15 @@ and repr_options_of_json (ctx : of_json_ctx) (js : json) :
             : repr_options)
     | _ -> Error "")
 
+and runtime_check_of_json (ctx : of_json_ctx) (js : json) :
+    (runtime_check, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `String "UbChecks" -> Ok UbChecks
+    | `String "OverflowChecks" -> Ok OverflowChecks
+    | `String "ContractChecks" -> Ok ContractChecks
+    | _ -> Error "")
+
 and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -1760,10 +1769,6 @@ and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result =
         let* x_1 = ty_of_json ctx x_1 in
         let* x_2 = box_of_json constant_expr_of_json ctx x_2 in
         Ok (Repeat (x_0, x_1, x_2))
-    | `Assoc [ ("ShallowInitBox", `List [ x_0; x_1 ]) ] ->
-        let* x_0 = operand_of_json ctx x_0 in
-        let* x_1 = ty_of_json ctx x_1 in
-        Ok (ShallowInitBox (x_0, x_1))
     | _ -> Error "")
 
 and scalar_value_of_json (ctx : of_json_ctx) (js : json) :

charon/Cargo.lock

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.169"
+version = "0.1.170"
 authors = [
     "Son Ho <hosonmarc@gmail.com>",
     "Guillaume Boisseau <nadrieril+git@gmail.com>",

charon/Cargo.toml

@@ -8,7 +8,7 @@
     rust-overlay = {
       # We pin a specific commit because we require a relatively recent version
       # and flake dependents don't look at our flake.lock.
-      url = "github:oxalica/rust-overlay/ab726555a9a72e6dc80649809147823a813fa95b";
+      url = "github:oxalica/rust-overlay/085bdbf5dde5477538e4c87d1684b6c6df56c0ad";
       inputs.nixpkgs.follows = "nixpkgs";
     };
     crane.url = "github:ipetkov/crane";