Merge pull request #1088 from soteria-tools/issue-982

Add `Extern` and `Intrinsic` body types

Author: Nadrieril

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.180"
+let supported_charon_version = "0.1.181"

charon-ml/src/GAst.ml

@@ -26,6 +26,18 @@ type trait_declaration_group = TraitDeclId.id g_declaration_group
 type trait_impl_group = TraitImplId.id g_declaration_group [@@deriving show]
 type mixed_declaration_group = item_id g_declaration_group [@@deriving show]
 
+(* Hand-written because the rust equivalent isn't generic *)
+type 'body body =
+  | Body of 'body gexpr_body
+  | TraitMethodWithoutDefault
+  | Extern of string
+  | Intrinsic of { name : string; arg_names : string list }
+  | TargetDispatch of (string * fun_decl_ref) list
+  | Opaque
+  | Missing
+  | Error of error
+[@@deriving show]
+
 (* Hand-written because the rust equivalent isn't generic *)
 type 'body gfun_decl = {
   def_id : FunDeclId.id;
@@ -34,7 +46,7 @@ type 'body gfun_decl = {
   signature : fun_sig;
   src : item_source;
   is_global_initializer : GlobalDeclId.id option;
-  body : 'body gexpr_body option;
+  body : 'body body;
 }
 [@@deriving show]
 

charon-ml/src/GAstOfJson.ml

@@ -20,8 +20,7 @@ let option_list_of_json of_json = list_of_json (option_of_json of_json)
 
 (* This is written by hand because the corresponding rust type is not type-generic. *)
 let rec gfun_decl_of_json
-    (body_of_json :
-      of_json_ctx -> json -> ('body gexpr_body option, string) result)
+    (body_of_json : of_json_ctx -> json -> ('body body, string) result)
     (ctx : of_json_ctx) (js : json) : ('body gfun_decl, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -84,8 +83,7 @@ and id_to_file_of_json (ctx : of_json_ctx) (js : json) :
    type-generic. Note: because of hash-cons deduplication, we must make sure to
    deserialize in the exact same order as the rust side. *)
 and gtranslated_crate_of_json
-    (body_of_json :
-      of_json_ctx -> json -> ('body gexpr_body option, string) result)
+    (body_of_json : of_json_ctx -> json -> ('body body, string) result)
     (js : json) : ('body gcrate, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -172,8 +170,7 @@ and gtranslated_crate_of_json
     | _ -> Error "")
 
 and gcrate_of_json
-    (body_of_json :
-      of_json_ctx -> json -> ('body gexpr_body option, string) result)
+    (body_of_json : of_json_ctx -> json -> ('body body, string) result)
     (js : json) : ('body gcrate, string) result =
   match js with
   | `Assoc [ ("charon_version", charon_version); ("translated", translated) ]

charon-ml/src/LlbcAst.ml

@@ -6,7 +6,7 @@ include GAst
 include Generated_LlbcAst
 
 type expr_body = block gexpr_body [@@deriving show]
-type fun_body = expr_body [@@deriving show]
+type fun_body = block body [@@deriving show]
 type fun_decl = block gfun_decl [@@deriving show]
 
 (** LLBC crate *)

charon-ml/src/LlbcAstUtils.ml

@@ -15,8 +15,8 @@ let fun_decl_list_from_crate (crate : crate) : fun_decl list =
     returns None *)
 let get_fun_args (fun_decl : fun_decl) : local list option =
   match fun_decl.body with
-  | Some body -> Some (GAstUtils.locals_get_input_vars body.locals)
-  | None -> None
+  | Body body -> Some (GAstUtils.locals_get_input_vars body.locals)
+  | _ -> None
 
 (** Check if a {!type:Charon.LlbcAst.statement} contains loops *)
 let block_has_loops (blk : block) : bool =
@@ -34,8 +34,8 @@ let block_has_loops (blk : block) : bool =
 (** Check if a {!type:Charon.LlbcAst.fun_decl} contains loops *)
 let fun_decl_has_loops (fd : fun_decl) : bool =
   match fd.body with
-  | Some body -> block_has_loops body.body
-  | None -> false
+  | Body body -> block_has_loops body.body
+  | _ -> false
 
 let crate_get_item_meta (m : crate) (id : item_id) : Types.item_meta option =
   match id with
@@ -91,7 +91,27 @@ class ['self] map_crate =
       let is_global_initializer =
         self#visit_option self#visit_global_decl_id env is_global_initializer
       in
-      let body = self#visit_option self#visit_expr_body env body in
+      let body =
+        match body with
+        | Body b -> Body (self#visit_expr_body env b)
+        | TraitMethodWithoutDefault -> TraitMethodWithoutDefault
+        | Extern sym -> Extern (self#visit_string env sym)
+        | Intrinsic { name; arg_names } ->
+            Intrinsic
+              {
+                name = self#visit_string env name;
+                arg_names = List.map (self#visit_string env) arg_names;
+              }
+        | TargetDispatch targets ->
+            TargetDispatch
+              (self#visit_list
+                 (fun env (tgt, fref) ->
+                   (self#visit_string env tgt, self#visit_fun_decl_ref env fref))
+                 env targets)
+        | Opaque -> Opaque
+        | Missing -> Missing
+        | Error err -> Error (self#visit_error env err)
+      in
       {
         def_id;
         item_meta;
@@ -218,7 +238,22 @@ class ['self] iter_crate =
       self#visit_fun_sig env signature;
       self#visit_item_source env src;
       self#visit_option self#visit_global_decl_id env is_global_initializer;
-      self#visit_option self#visit_expr_body env body
+      match body with
+      | Body b -> self#visit_expr_body env b
+      | TraitMethodWithoutDefault -> ()
+      | Extern sym -> self#visit_string env sym
+      | Intrinsic { name; arg_names } ->
+          self#visit_string env name;
+          List.iter (self#visit_string env) arg_names
+      | TargetDispatch targets ->
+          self#visit_list
+            (fun env (tgt, fref) ->
+              self#visit_string env tgt;
+              self#visit_fun_decl_ref env fref)
+            env targets
+      | Opaque -> ()
+      | Missing -> ()
+      | Error err -> self#visit_error env err
 
     method visit_declaration_group env (g : declaration_group) : unit =
       match g with

charon-ml/src/LlbcOfJson.ml

@@ -9,13 +9,38 @@ include GAstOfJson
 include Generated_LlbcOfJson
 
 let expr_body_of_json (ctx : of_json_ctx) (js : json) :
-    (expr_body option, string) result =
+    (fun_body, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Structured", body) ] ->
         let* body = gexpr_body_of_json block_of_json ctx body in
-        Ok (Some body)
-    | _ -> Ok None)
+        Ok (Body body)
+    | `Assoc [ ("Unstructured", _) ] ->
+        (* Some .llbc bodies are emitted in ULLBC mode (e.g. UNIT_METADATA). *)
+        Ok Opaque
+    | `String "TraitMethodWithoutDefault" -> Ok TraitMethodWithoutDefault
+    | `Assoc [ ("Extern", sym) ] ->
+        let* sym = string_of_json ctx sym in
+        Ok (Extern sym)
+    | `Assoc
+        [ ("Intrinsic", `Assoc [ ("name", name); ("arg_names", arg_names) ]) ]
+      ->
+        let* name = string_of_json ctx name in
+        let* arg_names = list_of_json string_of_json ctx arg_names in
+        Ok (Intrinsic { name; arg_names })
+    | `Assoc [ ("TargetDispatch", targets) ] ->
+        let* targets =
+          list_of_json
+            (key_value_pair_of_json string_of_json fun_decl_ref_of_json)
+            ctx targets
+        in
+        Ok (TargetDispatch targets)
+    | `String "Opaque" -> Ok Opaque
+    | `String "Missing" -> Ok Missing
+    | `Assoc [ ("Error", e) ] ->
+        let* e = error_of_json ctx e in
+        Ok (GAst.Error e)
+    | _ -> Error "")
 
 let crate_of_json (js : json) : (crate, string) result =
   gcrate_of_json expr_body_of_json js

charon-ml/src/OfJsonBasic.ml

@@ -13,29 +13,30 @@ let combine_error_msgs (js : json) (msg : string) (res : ('a, string) result) :
     ('a, string) result =
   match res with
   | Ok x -> Ok x
-  | Error e -> Error ("[" ^ msg ^ "]" ^ " failed on: " ^ show js ^ "\n\n" ^ e)
+  | Error e ->
+      Error ("[" ^ msg ^ "]" ^ " failed on: " ^ to_string js ^ "\n\n" ^ e)
 
 let bool_of_json (ctx : 'ctx) (js : json) : (bool, string) result =
   match js with
   | `Bool b -> Ok b
-  | _ -> Error ("bool_of_json: not a bool: " ^ show js)
+  | _ -> Error ("bool_of_json: not a bool: " ^ to_string js)
 
 let int_of_json (ctx : 'ctx) (js : json) : (int, string) result =
   match js with
   | `Int i -> Ok i
-  | _ -> Error ("int_of_json: not an int: " ^ show js)
+  | _ -> Error ("int_of_json: not an int: " ^ to_string js)
 
 let char_of_json (ctx : 'ctx) (js : json) : (Uchar.t, string) result =
   match js with
   | `String c ->
       if String.length c > 4 then
-        Error ("char_of_json: stricly more than four bytes in: " ^ show js)
+        Error ("char_of_json: stricly more than four bytes in: " ^ to_string js)
       else
         let uchar = String.get_utf_8_uchar c 0 in
         if Uchar.utf_decode_is_valid uchar then
           Ok (Uchar.utf_decode_uchar uchar)
-        else Error ("char_of_json: invalid UTF-8 character: " ^ show js)
-  | _ -> Error ("char_of_json: not a char: " ^ show js)
+        else Error ("char_of_json: invalid UTF-8 character: " ^ to_string js)
+  | _ -> Error ("char_of_json: not a char: " ^ to_string js)
 
 let rec of_json_list (a_of_json : 'ctx -> json -> ('a, string) result)
     (ctx : 'ctx) (jsl : json list) : ('a list, string) result =
@@ -54,7 +55,7 @@ let pair_of_json (a_of_json : 'ctx -> json -> ('a, string) result)
       let* a = a_of_json ctx a in
       let* b = b_of_json ctx b in
       Ok (a, b)
-  | _ -> Error ("pair_of_json failed on: " ^ show js)
+  | _ -> Error ("pair_of_json failed on: " ^ to_string js)
 
 let triple_of_json (a_of_json : 'ctx -> json -> ('a, string) result)
     (b_of_json : 'ctx -> json -> ('b, string) result)
@@ -66,19 +67,19 @@ let triple_of_json (a_of_json : 'ctx -> json -> ('a, string) result)
       let* b = b_of_json ctx b in
       let* c = c_of_json ctx c in
       Ok (a, b, c)
-  | _ -> Error ("triple_of_json failed on: " ^ show js)
+  | _ -> Error ("triple_of_json failed on: " ^ to_string js)
 
 let list_of_json (a_of_json : 'ctx -> json -> ('a, string) result) (ctx : 'ctx)
     (js : json) : ('a list, string) result =
   combine_error_msgs js "list_of_json"
     (match js with
     | `List jsl -> of_json_list a_of_json ctx jsl
-    | _ -> Error ("not a list: " ^ show js))
+    | _ -> Error ("not a list: " ^ to_string js))
 
 let string_of_json (ctx : 'ctx) (js : json) : (string, string) result =
   match js with
   | `String str -> Ok str
-  | _ -> Error ("string_of_json: not a string: " ^ show js)
+  | _ -> Error ("string_of_json: not a string: " ^ to_string js)
 
 let option_of_json (a_of_json : 'ctx -> json -> ('a, string) result)
     (ctx : 'ctx) (js : json) : ('a option, string) result =
@@ -105,4 +106,4 @@ let key_value_pair_of_json (a_of_json : 'ctx -> json -> ('a, string) result)
       let* a = a_of_json ctx a in
       let* b = b_of_json ctx b in
       Ok (a, b)
-  | _ -> Error ("key_value_pair_of_json failed on: " ^ show js)
+  | _ -> Error ("key_value_pair_of_json failed on: " ^ to_string js)

charon-ml/src/PrintGAst.ml

@@ -112,10 +112,38 @@ let gfun_decl_to_string (env : 'a fmt_env) (indent : string)
    * (we have access to a body) *)
   let sg = bound_fun_sig_of_decl def in
   match def.body with
-  | None ->
+  | Opaque ->
       fun_sig_with_name_to_string env indent indent_incr (Some "opaque")
         (Some name) None sg
-  | Some body ->
+  | Missing ->
+      fun_sig_with_name_to_string env indent indent_incr (Some "missing")
+        (Some name) None sg
+  | TraitMethodWithoutDefault ->
+      fun_sig_with_name_to_string env indent indent_incr
+        (Some "method_without_default_body") (Some name) None sg
+  | Extern sym ->
+      fun_sig_with_name_to_string env indent indent_incr
+        (Some ("extern:" ^ sym))
+        (Some name) None sg
+  | Intrinsic { name; _ } ->
+      fun_sig_with_name_to_string env indent indent_incr
+        (Some ("intrinsic:" ^ name))
+        (Some name) None sg
+  | TargetDispatch targets ->
+      let targets =
+        targets
+        |> List.map (fun (tgt, fref) ->
+               tgt ^ " => " ^ fun_decl_ref_to_string env fref)
+        |> String.concat ","
+      in
+      fun_sig_with_name_to_string env indent indent_incr
+        (Some ("target_dispatch(" ^ targets ^ ")"))
+        (Some name) None sg
+  | Error err ->
+      fun_sig_with_name_to_string env indent indent_incr
+        (Some ("error(\"" ^ err.msg ^ "\")"))
+        (Some name) None sg
+  | Body body ->
       (* Locally update the environment *)
       let locals = List.map (fun v -> (v.index, v.name)) body.locals.locals in
       let env = { env with locals } in

charon-ml/src/Substitute.ml

@@ -428,8 +428,8 @@ let block_substitute (subst : subst) (blk : block) : block =
 
 (** Apply a type substitution to a function body. Return the local variables and
     the body. *)
-let fun_body_substitute_in_body (subst : subst) (body : fun_body) :
-    local list * block =
+let expr_body_substitute (subst : subst) (body : expr_body) : local list * block
+    =
   let locals =
     List.map
       (fun (v : local) -> { v with local_ty = ty_substitute subst v.local_ty })

charon-ml/src/UllbcAst.ml

@@ -7,7 +7,7 @@ include GAst
 include Generated_UllbcAst
 
 type expr_body = blocks gexpr_body [@@deriving show]
-type fun_body = expr_body [@@deriving show]
+type fun_body = blocks body [@@deriving show]
 type fun_decl = blocks gfun_decl [@@deriving show]
 
 (** ULLBC crate *)