Defining two calling conventions for Core

* Normal_callconv: the original and default one, where the elaboration of C
  		   parameters are passed by pointers (to temporary objects
		   allocated and initialised by the caller).

* Inner_arg_callconv: used by CN, where the elaboration of C parameters are
  		      passed by value (except for the additional parameters of
		      variadic functions) and the temporary objects are allocated
		      by the callee in its body.

This commit updates the Core typing and runtime to support both
calling conventions.

backend/bmc/bmc_utils.ml

@@ -408,6 +408,7 @@ let set_uid_globs (gname, glb) =
 let set_uid file1 =
  ({
   main=    (file1.main);
+  calling_convention= (file1.calling_convention);
   tagDefs= (file1.tagDefs);
   stdlib=  (file1.stdlib);
   impl=    (file1.impl);

backend/common/pipeline.ml

@@ -240,7 +240,9 @@ let c_frontend_and_elaboration ?(cnnames=[]) (conf, io) (core_stdlib, core_impl)
      used more than once, we need to do reset here *)
   (* TODO(someday): find a better way *)
   Tags.reset_tagDefs ();
-  let core_file = Translation.translate core_stdlib core_impl ailtau_prog in
+  let calling_convention =
+    Core.(if Switches.has_switch SW_inner_arg_temps then Inner_arg_callconv else Normal_callconv) in
+  let core_file = Translation.translate core_stdlib calling_convention core_impl ailtau_prog in
   io.set_progress "ELABO" >>= fun () ->
   io.pass_message "Translation to Core completed!" >>= fun () ->
   return (Some cabs_tunit, Some (markers_env, ailtau_prog), core_file)
@@ -253,6 +255,7 @@ let core_frontend (conf, io) (core_stdlib, core_impl) ~filename =
         (* Tags.set_tagDefs "Pipeline.core_frontend" tagDefs; *)
         return {
            Core.main=   Some sym_main;
+           Core.calling_convention= Core.Normal_callconv; (* TODO *)
            Core.tagDefs= tagDefs;
            Core.stdlib= snd core_stdlib;
            Core.impl=   core_impl;
@@ -481,6 +484,7 @@ let untype_file (file: 'a Core.typed_file) : 'a Core.file =
     | GlobalDecl _ as glob ->
         glob in
   { main= file.main
+  ; calling_convention= file.calling_convention
   ; tagDefs= file.tagDefs
   ; stdlib= Pmap.map untype_generic_fun_map_decl file.stdlib
   ; impl= Pmap.map untype_generic_impl_decl file.impl
@@ -599,13 +603,14 @@ let interp_backend io core_file ~args ~batch ~fs ~driver_conf =
  * program, with exactly the same compiled code. *)
 type 'a core_dump =
   { dump_main: Symbol.sym option;
+    dump_calling_convention: Core.calling_convention;
     dump_tagDefs: (Symbol.sym * (Cerb_location.t * Ctype.tag_definition)) list;
     dump_globs: (Symbol.sym * ('a, unit) Core.generic_globs) list;
     dump_funs: (Symbol.sym * (unit, 'a) Core.generic_fun_map_decl) list;
     dump_extern: (Symbol.identifier * (Symbol.sym list * Core.linking_kind)) list;
     dump_funinfo: (Symbol.sym * (Cerb_location.t * Annot.attributes * Ctype.ctype * (Symbol.sym option * Ctype.ctype) list * bool * bool)) list;
-    dump_loop_attributes: (int * Annot.attributes) list;
-  } [@@warning "-unused-field"]
+    (* dump_loop_attributes: (int * Annot.attributes) list; *)
+  }
 
 let sym_compare (Symbol.Symbol (d1, n1, _)) (Symbol.Symbol (d2, n2, _)) =
   if d1 = d2 then compare n1 n2
@@ -630,9 +635,10 @@ let read_core_object (conf, io) ?(is_lib=false) (core_stdlib, core_impl) filenam
   if v <> version_info
   then
     Cerb_debug.warn [] (fun () -> "read core_object file produced with a different version of Cerberus => " ^ v);
-  let dump = Marshal.from_channel ic in
+  let dump: 'a core_dump = Marshal.from_channel ic in
   close_in ic;
-  let core_file = { main=    dump.main;
+  let core_file = { main=    dump.dump_main;
+    calling_convention= dump.dump_calling_convention;
     tagDefs= map_from_assoc sym_compare dump.dump_tagDefs;
     stdlib=  snd core_stdlib;
     impl=    core_impl;
@@ -650,14 +656,15 @@ let read_core_object (conf, io) ?(is_lib=false) (core_stdlib, core_impl) filenam
 
 let write_core_object core_file fname =
   let open Core in
-  let dump =
+  let dump: 'a core_dump =
     { dump_main = core_file.main;
+      dump_calling_convention = core_file.calling_convention;
       dump_tagDefs = Pmap.bindings_list core_file.tagDefs;
       dump_globs = core_file.globs;
       dump_funs = Pmap.bindings_list core_file.funs;
       dump_extern = Pmap.bindings_list core_file.extern;
       dump_funinfo = Pmap.bindings_list core_file.funinfo;
-      dump_loop_attributes = [] (*Pmap.bindings_list core_file.loop_attributes0*);
+(*      dump_loop_attributes = [] (*Pmap.bindings_list core_file.loop_attributes0*); *)
     }
   in
   let oc = open_out_bin fname in

backend/web/instance.ml

@@ -328,6 +328,7 @@ let set_uid file =
     )
   in
   { main=    file.main;
+    calling_convention= file.calling_convention;
     tagDefs= file.tagDefs;
     stdlib=  file.stdlib;
     impl=    file.impl;

frontend/model/core.lem

@@ -403,18 +403,27 @@ type core_tag_definitions =
 
 type visible_objects_env = map nat (list (Symbol.sym * Ctype.ctype))
 
+type calling_convention =
+  | Normal_callconv
+  | Inner_arg_callconv
+
+instance (Eq calling_convention)
+  let (=)  = unsafe_structural_equality
+  let (<>) = unsafe_structural_inequality
+end
 
 (* a Core file is just a set of named functions *)
 type generic_file 'bty 'a = <|
-  main    : maybe Symbol.sym;
-  tagDefs : core_tag_definitions;
-  stdlib  : generic_fun_map 'bty 'a;
-  impl    : generic_impl 'bty;
-  globs   : list (Symbol.sym * generic_globs 'a 'bty);
-  funs    : generic_fun_map 'bty 'a;
-  extern  : extern_map;
-  funinfo : map Symbol.sym (Loc.t * Annot.attributes * ctype * list (maybe Symbol.sym * ctype) * bool * bool);
-  loop_attributes : Annot.loop_attributes;
+  main: maybe Symbol.sym;
+  calling_convention: calling_convention;
+  tagDefs: core_tag_definitions;
+  stdlib: generic_fun_map 'bty 'a;
+  impl: generic_impl 'bty;
+  globs: list (Symbol.sym * generic_globs 'a 'bty);
+  funs: generic_fun_map 'bty 'a;
+  extern: extern_map;
+  funinfo: map Symbol.sym (Loc.t * Annot.attributes * ctype * list (maybe Symbol.sym * ctype) * bool * bool);
+  loop_attributes: Annot.loop_attributes;
   visible_objects_env: visible_objects_env;
 |>
 

frontend/model/core_linking.lem

@@ -281,10 +281,14 @@ val link_aux: forall 'a 'b. generic_file 'a 'b ->
                            generic_file 'a 'b ->
                            exceptM (generic_file 'a 'b) (Loc.t * cause)
 let link_aux f1 f2 =
+  if f1.calling_convention <> f2.calling_convention then
+    link_fail Loc.unknown IncompatibleCallingConvention
+  else
   link_extern f2.extern f1.extern >>= fun (extern, reduntant_globs) ->
   link_main f1.main f2.main >>= fun main ->
   return
     <| main=    main;
+       calling_convention= f1.calling_convention;
        tagDefs= f1.tagDefs union f2.tagDefs;
        stdlib=  f1.stdlib;
        impl=    f1.impl;

frontend/model/core_run_aux.lem

@@ -693,6 +693,7 @@ let convert_file file =
 
  <|
   main=    file.main;
+  calling_convention= file.calling_convention;
   tagDefs= file.tagDefs;
   stdlib=  Map.map convert_fun_map_decl file.stdlib;
   impl=    Map.map convert_impl_decl file.impl;

frontend/model/core_typing.lem

@@ -1630,9 +1630,21 @@ let rec collect_labels env (Expr _ expr_) =
 
 
 (* val     typecheck_expr: Loc.t -> typing_env -> core_base_type -> Core.expr unit -> E.eff (typed_expr unit) *)
-and typecheck_expr tagDefs (env: typing_env) expected_bTy (Expr annot expr_) =
-  let typecheck_expr env expected_bTy expr = typecheck_expr tagDefs env expected_bTy expr in
+and typecheck_expr callconv tagDefs (env: typing_env) expected_bTy (Expr annot expr_) =
+  let typecheck_expr env expected_bTy expr = typecheck_expr callconv tagDefs env expected_bTy expr in
   let loc = Annot.get_loc_ annot in
+  let typecheck_ccall_argument =
+    match callconv with
+      | Normal_callconv ->
+          fun _ pe -> typecheck_export_pexpr tagDefs env (BTy_object OTy_pointer) pe
+      | Inner_arg_callconv ->
+          fun ty pe -> match Core_aux.core_object_type_of_ctype ty with
+            | Just oTy ->
+                typecheck_export_pexpr tagDefs env (BTy_loaded oTy) pe
+            | Nothing ->
+                E.fail loc (CoreTyping_TODO "the first operand of ccall() has a C function type with a non object parameter type")
+          end
+    end in
   Expr annot <$> match expr_ with
     | Epure pe ->
         Epure <$> typecheck_export_pexpr tagDefs env expected_bTy pe
@@ -1676,43 +1688,46 @@ and typecheck_expr tagDefs (env: typing_env) expected_bTy (Expr annot expr_) =
         Eif <$> typecheck_export_pexpr tagDefs env BTy_boolean pe1
             <*> typecheck_expr env expected_bTy e2
             <*> typecheck_expr env expected_bTy e3
-    | Eccall annot pe_ty pe pes ->
-        infer_pexpr tagDefs env pe_ty >>= export_pexpr >>= fun pe_ty' ->
+    | Eccall annot ty_pe pe pes ->
+        infer_pexpr tagDefs env ty_pe >>= export_pexpr >>= fun ty_pe' ->
         infer_pexpr tagDefs env pe    >>= export_pexpr >>= fun (Pexpr _ bTy _ as pe') ->
-        match (pe_ty, bTy) with
-          | (Pexpr _ _ (PEval (Vctype (Cty.Ctype _ (Cty.Pointer _ (Cty.Ctype _ (Cty.Function (qs, ty) params isVariadic))))))
-            , BTy_loaded OTy_pointer) ->
+        match (ty_pe, bTy) with
+          | ( Pexpr _ _ (PEval (Vctype (Cty.Ctype _ (Cty.Pointer _ (Cty.Ctype _ (Cty.Function (qs, ty) params isVariadic))))))
+            , BTy_loaded OTy_pointer ) ->
               begin
                 if isVariadic then
                   match List.dest_init pes with
                     | Nothing ->
                         E.fail loc (CoreTyping_TODO "ccall to a variadic C procedure must at least have a list of pointers as last argument")
-                    | Just (first_pes, last_pe) ->
-                        E.mapM (fun pe ->
-                          typecheck_export_pexpr tagDefs env (BTy_object OTy_pointer) pe
-                        ) first_pes >>= fun first_pes' ->
+                    | Just (xs, last_pe) ->
+                        E.mapM (fun ((_, ty, _), pe) ->
+                          typecheck_ccall_argument ty pe
+                        ) (List.zip params pes) >>= fun pes' ->
                         typecheck_export_pexpr tagDefs env
                           (BTy_list (BTy_tuple [BTy_ctype; BTy_object OTy_pointer])) last_pe >>= fun last_pe' ->
-                        E.return (first_pes' ++ [last_pe'])
+                        E.return (pes' ++ [last_pe'])
                   end
                 else
-                  if Global.has_switch Global.SW_inner_arg_temps then
-                    E.mapM (fun ((_, ty, _), pe) ->
-                      match Core_aux.core_object_type_of_ctype ty with
-                        | Just oTy ->
-                            typecheck_export_pexpr tagDefs env (BTy_loaded oTy) pe
-                        | Nothing ->
-                            E.fail loc (CoreTyping_TODO "the first operand of ccall() has a C function type with a non object parameter type")
-                      end
-                    ) (List.zip params pes)
-                  else
-                    E.mapM (fun pe ->
-                      typecheck_export_pexpr tagDefs env (BTy_object OTy_pointer) pe
-                    ) pes
+                  E.mapM (fun ((_, ty, _), pe) -> typecheck_ccall_argument ty pe) (List.zip params pes)
+                (* else match callconv with
+                  | Normal_callconv ->
+                      E.mapM (fun pe ->
+                        typecheck_export_pexpr tagDefs env (BTy_object OTy_pointer) pe
+                      ) pes
+                  | Inner_arg_callconv ->
+                      E.mapM (fun ((_, ty, _), pe) ->
+                        match Core_aux.core_object_type_of_ctype ty with
+                          | Just oTy ->
+                              typecheck_export_pexpr tagDefs env (BTy_loaded oTy) pe
+                          | Nothing ->
+                              E.fail loc (CoreTyping_TODO "the first operand of ccall() has a C function type with a non object parameter type")
+                        end
+                      ) (List.zip params pes)
+                end *)
               end >>= fun pes' ->
               let ret_oTy_opt = Core_aux.core_object_type_of_ctype ty in
               guard_match loc "ccall" expected_bTy (maybe BTy_unit BTy_loaded ret_oTy_opt) >>
-              E.return (Eccall annot pe_ty' pe' pes')
+              E.return (Eccall annot ty_pe' pe' pes')
           | (_, _) ->
               E.fail loc (CoreTyping_TODO "the first operand of ccall() should have a C function type")
         end
@@ -1819,6 +1834,8 @@ and typecheck_expr tagDefs (env: typing_env) expected_bTy (Expr annot expr_) =
 (* TODO: add a check for the existence of main *)
 val typecheck_program: forall 'bty 'a. Core.generic_file 'bty 'a -> Exception.exceptM (Core.typed_file 'a) Errors.error
 let typecheck_program file =
+  let typecheck_expr env expected_bTy expr =
+    typecheck_expr file.calling_convention file.tagDefs env expected_bTy expr in
   let aux =
     (* The startup function/procedure must be defined *)
     match file.main with
@@ -1866,7 +1883,7 @@ let typecheck_program file =
         | Proc loc mrk bTy sym_bTys e ->
             let env' = List.foldr (fun (sym, bTy) acc -> insert_tdecl (Sym sym) (TDsym bTy) acc) env sym_bTys in
             collect_labels env' e >>= fun env' ->
-            Proc loc mrk bTy sym_bTys <$> typecheck_expr file.tagDefs env' bTy e
+            Proc loc mrk bTy sym_bTys <$> typecheck_expr env' bTy e
       end) file.stdlib >>= fun stdlib' ->
 
     (* Typechecking of the impl constants *)
@@ -1884,7 +1901,7 @@ let typecheck_program file =
       match decl with
         | GlobalDef (bTy, ct) e ->
             collect_labels env_acc e >>= fun env_acc' ->
-            typecheck_expr file.tagDefs env_acc' bTy e >>= fun te ->
+            typecheck_expr env_acc' bTy e >>= fun te ->
             E.return (insert_tdecl (Sym sym) (TDsym bTy) env_acc', (sym, GlobalDef (bTy, ct) te) :: acc)
         | GlobalDecl (bTy, ct) ->
             E.return (insert_tdecl (Sym sym) (TDsym bTy) env_acc, (sym, GlobalDecl (bTy, ct)) :: acc)
@@ -1919,11 +1936,12 @@ let typecheck_program file =
         | Proc loc mrk bTy sym_bTys e ->
             let env' = List.foldr (fun (sym, bTy) acc -> insert_tdecl (Sym sym) (TDsym bTy) acc) env sym_bTys in
             collect_labels env' e >>= fun env' ->
-            Proc loc mrk bTy sym_bTys <$> typecheck_expr file.tagDefs env' bTy e
+            Proc loc mrk bTy sym_bTys <$> typecheck_expr env' bTy e
       end) file.funs >>= fun funs' ->
 
     E.return <|
       main= file.main;
+      calling_convention = file.calling_convention;
       tagDefs= file.tagDefs;
       stdlib= stdlib';
       impl= impl';

frontend/model/ctype.lem

@@ -381,6 +381,10 @@ val ptrdiff_t: ctype
 let ptrdiff_t =
   Ctype [] (Basic (Integer Ptrdiff_t))
 
+val pointer_to_char: ctype
+let pointer_to_char =
+  Ctype [] (Pointer no_qualifiers char)
+
 import Global
 val ptraddr_t: unit -> ctype
 let ptraddr_t _ =