Simpler, more robust emulation of calls to variadic functions:

- C function types and Cminor signatures annotated by calling conventions.
  esp. vararg / not vararg
- Cshmgen: generate correct code for function call where there are
  more arguments than listed in the function prototype.  This is
  still undefined behavior according to the formal semantics,
  but correct code is generated.
- C2C, */PrintAsm.ml: remove "printf$iif" hack.
- powerpc/, checklink/: don't generate stubs for variadic functions.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 33 insertions, 140 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index c51e090..8e8afd1 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -195,13 +195,10 @@ let mark_covered_fun_sym_ndx (ndx: int) ffw: f_framework =
   )
   >>> (ff_sf ^%= check_fun_symtab ffw.this_ident ndx)
 
-(** Taken from CompCert *)
-let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$"
-
 (** Tries to refine the mapping for key [k] in [ident_to_sym_ndx] so that it is
     mapped to [vaddr]. Fails if no symbol in [k]'s mapping has that virtual
-    address, unless the symbol is a stub from CompCert. Otherwise, it filters
-    out all symbols whose virtual address does not match [vaddr].
+    address. Otherwise, it filters out all symbols whose virtual
+    address does not match [vaddr].
 *)
 let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework)
     : s_framework or_err =
@@ -215,39 +212,16 @@ let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework)
     with
     | [] ->
         (* no symbol has that virtual address *)
-        let ident_name = Hashtbl.find sfw.ident_to_name k in
-        if Str.string_match re_variadic_stub ident_name 0
-        then (* this ident needs a stub, whose address is [vaddr] *)
-          try (
-            (* fetch the registered virtual address for this stub *)
-            let v = PosMap.find k sfw.stub_ident_to_vaddr in
-            (* if there is one, we're good if it's the same as [vaddr] *)
-            if vaddr = v
-            then OK(sfw)
-            else ERR(
-              Printf.sprintf
-                "Incoherent constraints for stub: %s"
-                (Hashtbl.find sfw.ident_to_name k)
-            )
-          )
-          with Not_found ->
-            (* if the stub has no previously registered virtual address,
-               register [vaddr] *)
-            OK(
-              sfw
-              >>> (stub_ident_to_vaddr ^%= PosMap.add k vaddr)
+        ERR(
+          Printf.sprintf
+            "Incoherent constraints for ident %s with value %s and candidates [%s]"
+            (Hashtbl.find sfw.ident_to_name k)
+            (string_of_int32 vaddr)
+            (string_of_list
+               (fun ndx -> string_of_int32 sfw.ef.elf.e_symtab.(ndx).st_value)
+               ", " id_ndxes
             )
-        else (* not a stub, so this is a real error *)
-          ERR(
-            Printf.sprintf
-              "Incoherent constraints for ident %s with value %s and candidates [%s]"
-              (Hashtbl.find sfw.ident_to_name k)
-              (string_of_int32 vaddr)
-              (string_of_list
-                 (fun ndx -> string_of_int32 sfw.ef.elf.e_symtab.(ndx).st_value)
-                 ", " id_ndxes
-              )
-          )
+        )
     | ndxes ->
         if id_ndxes = ndxes
         then OK(sfw)
@@ -595,6 +569,20 @@ let rec match_jmptbl lbllist vaddr size ffw =
       end
   end
 
+(** Matches [ecode] against the expected CR6 magic before a function call.
+*)
+let match_set_cr6 sg ecode =
+  if sg.sig_cc.cc_vararg then
+    if List.mem Tfloat sg.sig_args then
+      match ecode with
+      | CREQV(6, 6, 6) :: ecode' -> Some ecode'
+      | _ -> None
+    else
+      match ecode with
+      | CRXOR(6, 6, 6) :: ecode' -> Some ecode'
+      | _ -> None
+  else Some ecode
+
 (** Matches [ecode] agains the expected code for a small memory copy
     pseudo-instruction. Returns a triple containing the updated framework,
     the remaining ELF code, and the updated program counter.
@@ -1022,8 +1010,8 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
           | _ -> error
           end
       | Pbctr sg ->
-          begin match ecode with
-          | BCCTRx(bo, bi, lk) :: es ->
+          begin match match_set_cr6 sg ecode with
+          | Some(BCCTRx(bo, bi, lk) :: es) ->
               OK(fw)
               >>= match_bo_ctr bo
               >>= match_ints  0     bi
@@ -1032,8 +1020,8 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
           | _ -> error
           end
       | Pbctrl sg ->
-          begin match ecode with
-          | BCCTRx(bo, bi, lk) :: es ->
+          begin match match_set_cr6 sg ecode with
+          | Some(BCCTRx(bo, bi, lk) :: es) ->
               OK(fw)
               >>= match_bo_ctr bo
               >>= match_ints  0    bi
@@ -1070,8 +1058,8 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
           | _ -> error
           end
       | Pbl(ident, sg) ->
-          begin match ecode with
-          | Bx(li, aa, lk) :: es ->
+          begin match match_set_cr6 sg ecode with
+          | Some(Bx(li, aa, lk) :: es) ->
               let dest = Int32.(add pc (mul 4l (exts li))) in
               OK(fw)
               >>= (ff_sf ^%=? idmap_unify ident dest)
@@ -1091,8 +1079,8 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
           | _ -> error
           end
       | Pbs(ident, sg) ->
-          begin match ecode with
-          | Bx(li, aa, lk) :: es ->
+          begin match match_set_cr6 sg ecode with
+          | Some(Bx(li, aa, lk) :: es) ->
               let dest = Int32.(add pc (mul 4l (exts li))) in
               OK(fw)
               >>= match_bools false aa
@@ -2911,87 +2899,6 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework)
     (* Empty lists mean the symbol is external, no need for check *)
     (List.filter (fun (_, gv) -> gv.gvar_init <> []) pv)
 
-(** Checks that everything that has been assimiled as a stub during checks
-    indeed looks like a stub.
-*)
-let check_stubs sfw =
-  let check cond msg sfw =
-    sfw
-    >>> (if cond then id else (sf_ef ^%= add_log (ERROR(msg))))
-  in
-  let check_eq msg a b = check (a = b) msg in
-  let match_bools = check_eq "match_bools" in
-  let match_ints = check_eq "match_ints" in
-  let check_stub ident vaddr sfw =
-    let fundef = List.find (fun (i, _) -> i = ident) sfw.program.prog_defs in
-    let elf = sfw.ef.elf in
-    let stub_ecode = from_some (code_at_vaddr elf vaddr 2) in
-    let stub_offset = from_some (physical_offset_of_vaddr elf vaddr) in
-    begin match fundef with
-    | (_, Gfun(External(EF_external(dest_ident, _) as ef))) ->
-        let args = (ef_sig ef).sig_args in
-        if List.mem Tfloat args
-        then
-          begin match stub_ecode with
-          |   CREQV(crbD, crbA, crbB) :: (* vaddr *)
-              Bx(li, aa, lk)          :: (* vaddr + 4 *)
-              [] ->
-              let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in
-              begin match idmap_unify dest_ident dest_vaddr sfw with
-              | ERR(s) ->
-                  sfw
-                  >>> (sf_ef ^%= add_log (ERROR(
-                    "Couldn't match stub, " ^ s
-                  )))
-              | OK(sfw) ->
-                  sfw
-                  >>> match_ints 6 crbD
-                  >>> match_ints 6 crbA
-                  >>> match_ints 6 crbB
-                  >>> match_bools false aa
-                  >>> match_bools false lk
-                  >>> (sf_ef ^%=
-                      add_range stub_offset 8l 4
-                        (Stub(Hashtbl.find sfw.ident_to_name ident))
-                  )
-              end
-          | _ ->
-              sfw
-              >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub")))
-          end
-        else
-          begin match stub_ecode with
-          |   CRXOR(crbD, crbA, crbB) :: (* vaddr *)
-              Bx(li, aa, lk)          :: (* vaddr + 4 *)
-              [] ->
-              let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in
-              begin match idmap_unify dest_ident dest_vaddr sfw with
-              | ERR(s) ->
-                  sfw
-                  >>> (sf_ef ^%= add_log (ERROR(
-                    "Couldn't match stub, " ^ s
-                  )))
-              | OK(sfw) ->
-                  sfw
-                  >>> match_ints 6 crbD
-                  >>> match_ints 6 crbA
-                  >>> match_ints 6 crbB
-                  >>> match_bools false aa
-                  >>> match_bools false lk
-                  >>> (sf_ef ^%=
-                      add_range stub_offset 8l 4
-                        (Stub(Hashtbl.find sfw.ident_to_name ident))
-                  )
-              end
-          | _ ->
-              sfw
-              >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub")))
-          end
-    | _ -> fatal "Unexpected fundef in check_stubs, please report."
-    end
-  in
-  PosMap.fold check_stub sfw.stub_ident_to_vaddr sfw
-
 (** Read a .sdump file *)
 
 let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version
@@ -3065,17 +2972,11 @@ let process_sdump efw sdump: e_framework =
     ; program             = prog
     ; ident_to_name       = names
     ; ident_to_sym_ndx    = ident_to_sym_ndx
-    ; stub_ident_to_vaddr = PosMap.empty
     ; atoms               = atoms
     }
   )
   >>> worklist_process wl
   >>> (fun sfw ->
-    print_debug "Checking stubs";
-    sfw
-  )
-  >>> check_stubs
-  >>> (fun sfw ->
     print_debug "Checking data";
     sfw
   )
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index 35144dc..ec11412 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -84,9 +84,6 @@ type s_framework = {
       as we learn more about the contents of the symbol.
   *)
   ident_to_sym_ndx: (int list) PosMap.t;
-  (** CompCert generates stubs for some functions, which we will aggregate as we
-      discover them. *)
-  stub_ident_to_vaddr: int32 PosMap.t;
   (** This structure is imported from CompCert's .sdump, and describes each
       atom. *)
   atoms: (ident, C2C.atom_info) Hashtbl.t;
@@ -140,11 +137,6 @@ let ident_to_sym_ndx = {
   set = (fun i sf -> { sf with ident_to_sym_ndx = i });
 }
 
-let stub_ident_to_vaddr = {
-  get = (fun sf -> sf.stub_ident_to_vaddr);
-  set = (fun i sf -> { sf with stub_ident_to_vaddr = i });
-}
-
 (** Adds a range to the checked bytes list.
 *)
 let add_range (start: int32) (length: int32) (align: int) (bcd: byte_chunk_desc)