Merge pull request #1095 from Nadrieril/multi-target

Support multi-target compilation

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.178"
+let supported_charon_version = "0.1.179"

charon-ml/src/GAst.ml

@@ -47,7 +47,7 @@ type target_info = { target_pointer_size : int; is_little_endian : bool }
 type 'fun_body gcrate = {
   name : string;
   options : cli_options;
-  target_information : target_info;
+  target_information : (string * target_info) list;
   declarations : declaration_group list;
   type_decls : type_decl TypeDeclId.Map.t;
   fun_decls : 'fun_body gfun_decl FunDeclId.Map.t;

charon-ml/src/GAstOfJson.ml

@@ -112,7 +112,11 @@ and gtranslated_crate_of_json
 
         let* crate_name = string_of_json ctx crate_name in
         let* options = cli_options_of_json ctx options in
-        let* target_information = target_info_of_json ctx target_info in
+        let* target_information =
+          list_of_json
+            (key_value_pair_of_json string_of_json target_info_of_json)
+            ctx target_info
+        in
         let* _item_names =
           list_of_json
             (key_value_pair_of_json item_id_of_json name_of_json)
@@ -140,14 +144,17 @@ and gtranslated_crate_of_json
         in
         let* unit_metadata = global_decl_ref_of_json ctx unit_metadata in
         let* ordered_decls =
-          list_of_json declaration_group_of_json ctx ordered_decls
+          option_of_json
+            (list_of_json declaration_group_of_json)
+            ctx ordered_decls
         in
 
         let type_decls = TypeDeclId.map_of_indexed_list type_decls in
         let fun_decls = FunDeclId.map_of_indexed_list fun_decls in
         let global_decls = GlobalDeclId.map_of_indexed_list global_decls in
         let trait_decls = TraitDeclId.map_of_indexed_list trait_decls in
         let trait_impls = TraitImplId.map_of_indexed_list trait_impls in
+        let ordered_decls = Option.value ordered_decls ~default:[] in
 
         Ok
           {

charon-ml/src/GAstUtils.ml

@@ -2,6 +2,12 @@ open Types
 open TypesUtils
 open GAst
 
+let get_target_information crate =
+  match crate.target_information with
+  | [ (_, info) ] -> info
+  | _ ->
+      failwith "`get_target_information` can't be used in a multi-layout crate"
+
 (** Small utility: list the transitive parents of a region var group. We don't
     do that in an efficient manner, but it doesn't matter.
 

charon-ml/src/LlbcAstUtils.ml

@@ -153,7 +153,11 @@ class ['self] map_crate =
       in
       let name = self#visit_string env name in
       let options = self#visit_cli_options env options in
-      let target_information = self#visit_target_info env target_information in
+      let target_information =
+        List.map
+          (fun (name, info) -> (name, self#visit_target_info env info))
+          target_information
+      in
       let declarations =
         List.map (self#visit_declaration_group env) declarations
       in

charon-ml/src/NameMatcher.ml

@@ -978,7 +978,7 @@ and path_elem_with_generic_args_to_pattern (ctx : 'fun_body ctx)
       | Some args -> [ PIdent (s, d, args) ]
     end
   | PeImpl impl -> [ impl_elem_to_pattern ctx c impl ]
-  | PeInstantiated _ ->
+  | PeInstantiated _ | PeTarget _ ->
       (* In pattern generation, we skip monomorphized elements since patterns
          are meant to match the logical structure, not the instantiation details *)
       []

charon-ml/src/PrintTypes.ml

@@ -480,6 +480,7 @@ and path_elem_to_string (env : 'a fmt_env) (e : path_elem) : string =
       let env = fmt_env_push_generics_and_preds env binder.binder_params in
       let explicits, _ = generic_args_to_strings env binder.binder_value in
       "<" ^ String.concat ", " explicits ^ ">"
+  | PeTarget target -> target
 
 and name_to_string (env : 'a fmt_env) (n : name) : string =
   let name = List.map (path_elem_to_string env) n in

charon-ml/src/TypesUtils.ml

@@ -320,7 +320,11 @@ let generic_params_lengths (args : generic_params) : int * int * int * int =
     variant[TagEncoding::Niche::untagged_variant]. *)
 let get_variant_from_tag ptr_size ty_decl (tag : Values.scalar_value) =
   let ( let* ) = Option.bind in
-  let* layout = ty_decl.layout in
+  let layout =
+    match ty_decl.layout with
+    | [ (_, layout) ] -> layout
+    | _ -> failwith "get_variant_from_tag can't be used in a multi-layout crate"
+  in
   let* discr_layout = layout.discriminant_layout in
   match ty_decl.kind with
   | Enum variants -> begin

charon-ml/src/generated/Generated_GAst.ml

@@ -402,6 +402,11 @@ type cli_options = {
       (** The MIR stage to extract. This is only relevant for the current crate;
           for dpendencies only MIR optimized is available. *)
   rustc_args : string list;  (** Extra flags to pass to rustc. *)
+  targets : string list;
+      (** A list of target architectures to translate for. Charon will run the
+          compiler once for each target and aggregate the results, which is
+          useful if the code includes [#[cfg(..)]] filters. Warning: this is an
+          initial implementation which is extremely slow. *)
   monomorphize : bool;
       (** Monomorphize the items encountered when possible. Generic items found
           in the crate are skipped. To only translate a particular call graph,

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -414,6 +414,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
           ("skip_borrowck", skip_borrowck);
           ("mir", mir);
           ("rustc_args", rustc_args);
+          ("targets", targets);
           ("monomorphize", monomorphize);
           ("monomorphize_mut", monomorphize_mut);
           ("start_from", start_from);
@@ -456,6 +457,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
         let* skip_borrowck = bool_of_json ctx skip_borrowck in
         let* mir = option_of_json mir_level_of_json ctx mir in
         let* rustc_args = list_of_json string_of_json ctx rustc_args in
+        let* targets = list_of_json string_of_json ctx targets in
         let* monomorphize = bool_of_json ctx monomorphize in
         let* monomorphize_mut =
           option_of_json monomorphize_mut_of_json ctx monomorphize_mut
@@ -515,6 +517,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
              skip_borrowck;
              mir;
              rustc_args;
+             targets;
              monomorphize;
              monomorphize_mut;
              start_from;
@@ -1006,17 +1009,17 @@ and generic_args_of_json (ctx : of_json_ctx) (js : json) :
           ("trait_refs", trait_refs);
         ] ->
         let* regions =
-          index_map_of_json region_id_of_json region_of_json ctx regions
+          indexed_map_of_json region_id_of_json region_of_json ctx regions
         in
         let* types =
-          index_map_of_json type_var_id_of_json ty_of_json ctx types
+          indexed_map_of_json type_var_id_of_json ty_of_json ctx types
         in
         let* const_generics =
-          index_map_of_json const_generic_var_id_of_json constant_expr_of_json
+          indexed_map_of_json const_generic_var_id_of_json constant_expr_of_json
             ctx const_generics
         in
         let* trait_refs =
-          index_map_of_json trait_clause_id_of_json trait_ref_of_json ctx
+          indexed_map_of_json trait_clause_id_of_json trait_ref_of_json ctx
             trait_refs
         in
         Ok ({ regions; types; const_generics; trait_refs } : generic_args)
@@ -1037,17 +1040,17 @@ and generic_params_of_json (ctx : of_json_ctx) (js : json) :
           ("trait_type_constraints", trait_type_constraints);
         ] ->
         let* regions =
-          index_map_of_json region_id_of_json region_param_of_json ctx regions
+          indexed_map_of_json region_id_of_json region_param_of_json ctx regions
         in
         let* types =
-          index_map_of_json type_var_id_of_json type_param_of_json ctx types
+          indexed_map_of_json type_var_id_of_json type_param_of_json ctx types
         in
         let* const_generics =
-          index_map_of_json const_generic_var_id_of_json
+          indexed_map_of_json const_generic_var_id_of_json
             const_generic_param_of_json ctx const_generics
         in
         let* trait_clauses =
-          index_map_of_json trait_clause_id_of_json trait_param_of_json ctx
+          indexed_map_of_json trait_clause_id_of_json trait_param_of_json ctx
             trait_clauses
         in
         let* regions_outlive =
@@ -1063,7 +1066,7 @@ and generic_params_of_json (ctx : of_json_ctx) (js : json) :
             ctx types_outlive
         in
         let* trait_type_constraints =
-          index_map_of_json trait_type_constraint_id_of_json
+          indexed_map_of_json trait_type_constraint_id_of_json
             (region_binder_of_json trait_type_constraint_of_json)
             ctx trait_type_constraints
         in
@@ -1156,7 +1159,7 @@ and impl_elem_of_json (ctx : of_json_ctx) (js : json) :
         Ok (ImplElemTrait trait)
     | _ -> Error "")
 
-and index_map_of_json :
+and indexed_map_of_json :
     'a0 'a1.
     (of_json_ctx -> json -> ('a0, string) result) ->
     (of_json_ctx -> json -> ('a1, string) result) ->
@@ -1171,6 +1174,21 @@ and index_map_of_json :
         Ok (List.filter_map (fun x -> x) list)
     | _ -> Error "")
 
+and index_map_of_json :
+    'a0 'a1 'a2.
+    (of_json_ctx -> json -> ('a0, string) result) ->
+    (of_json_ctx -> json -> ('a1, string) result) ->
+    (of_json_ctx -> json -> ('a2, string) result) ->
+    of_json_ctx ->
+    json ->
+    (('a0 * 'a1) list, string) result =
+ fun arg0_of_json arg1_of_json arg2_of_json ctx js ->
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | json ->
+        list_of_json (key_value_pair_of_json arg0_of_json arg1_of_json) ctx json
+    | _ -> Error "")
+
 and index_vec_of_json :
     'a0 'a1.
     (of_json_ctx -> json -> ('a0, string) result) ->
@@ -1314,7 +1332,7 @@ and item_source_of_json (ctx : of_json_ctx) (js : json) :
           index_vec_of_json field_id_of_json v_table_field_of_json ctx field_map
         in
         let* supertrait_map =
-          index_map_of_json trait_clause_id_of_json
+          indexed_map_of_json trait_clause_id_of_json
             (option_of_json field_id_of_json)
             ctx supertrait_map
         in
@@ -1538,6 +1556,9 @@ and path_elem_of_json (ctx : of_json_ctx) (js : json) :
           box_of_json (binder_of_json generic_args_of_json) ctx instantiated
         in
         Ok (PeInstantiated instantiated)
+    | `Assoc [ ("Target", target) ] ->
+        let* target = string_of_json ctx target in
+        Ok (PeTarget target)
     | _ -> Error "")
 
 and place_of_json (ctx : of_json_ctx) (js : json) : (place, string) result =
@@ -1671,7 +1692,7 @@ and region_binder_of_json :
     (match js with
     | `Assoc [ ("regions", regions); ("skip_binder", skip_binder) ] ->
         let* binder_regions =
-          index_map_of_json region_id_of_json region_param_of_json ctx regions
+          indexed_map_of_json region_id_of_json region_param_of_json ctx regions
         in
         let* binder_value = arg0_of_json ctx skip_binder in
         Ok ({ binder_regions; binder_value } : _ region_binder)
@@ -1884,7 +1905,7 @@ and trait_assoc_ty_of_json (ctx : of_json_ctx) (js : json) :
         let* attr_info = attr_info_of_json ctx attr_info in
         let* default = option_of_json trait_assoc_ty_impl_of_json ctx default in
         let* implied_clauses =
-          index_map_of_json trait_clause_id_of_json trait_param_of_json ctx
+          indexed_map_of_json trait_clause_id_of_json trait_param_of_json ctx
             implied_clauses
         in
         Ok ({ name; attr_info; default; implied_clauses } : trait_assoc_ty)
@@ -1925,7 +1946,7 @@ and trait_decl_of_json (ctx : of_json_ctx) (js : json) :
         let* item_meta = item_meta_of_json ctx item_meta in
         let* generics = generic_params_of_json ctx generics in
         let* implied_clauses =
-          index_map_of_json trait_clause_id_of_json trait_param_of_json ctx
+          indexed_map_of_json trait_clause_id_of_json trait_param_of_json ctx
             implied_clauses
         in
         let* consts = list_of_json trait_assoc_const_of_json ctx consts in
@@ -1988,7 +2009,7 @@ and trait_impl_of_json (ctx : of_json_ctx) (js : json) :
         let* impl_trait = trait_decl_ref_of_json ctx impl_trait in
         let* generics = generic_params_of_json ctx generics in
         let* implied_trait_refs =
-          index_map_of_json trait_clause_id_of_json trait_ref_of_json ctx
+          indexed_map_of_json trait_clause_id_of_json trait_ref_of_json ctx
             implied_trait_refs
         in
         let* consts =
@@ -2131,7 +2152,7 @@ and trait_ref_kind_of_json (ctx : of_json_ctx) (js : json) :
         ] ->
         let* builtin_data = builtin_impl_data_of_json ctx builtin_data in
         let* parent_trait_refs =
-          index_map_of_json trait_clause_id_of_json trait_ref_of_json ctx
+          indexed_map_of_json trait_clause_id_of_json trait_ref_of_json ctx
             parent_trait_refs
         in
         let* types =
@@ -2244,7 +2265,9 @@ and type_decl_of_json (ctx : of_json_ctx) (js : json) :
         let* generics = generic_params_of_json ctx generics in
         let* src = item_source_of_json ctx src in
         let* kind = type_decl_kind_of_json ctx kind in
-        let* layout = option_of_json layout_of_json ctx layout in
+        let* layout =
+          index_map_of_json string_of_json layout_of_json int_of_json ctx layout
+        in
         let* ptr_metadata = ptr_metadata_of_json ctx ptr_metadata in
         let* repr = option_of_json repr_options_of_json ctx repr in
         Ok