Merge branch 'master' into atomic-builtins

10 files changed, 78 insertions, 26 deletions

diff --git a/backend/RTL.v b/backend/RTL.v
index 56a5efeb..3cd4335d 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -104,8 +104,7 @@ Record function: Type := mkfunction {
     for its stack-allocated activation record.  [fn_params] is the list
     of registers that are bound to the values of arguments at call time.
     [fn_entrypoint] is the node of the first instruction of the function
-    in the CFG.  [fn_code_wf] asserts that all instructions of the function
-    have nodes no greater than [fn_nextpc]. *)
+    in the CFG. *)
 
 Definition fundef := AST.fundef function.
 
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index d818de58..3da961c6 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -415,11 +415,12 @@ Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list
       a1' :: convert_builtin_args al rl1
   end.
 
-Definition convert_builtin_res (map: mapping) (r: builtin_res ident) : mon (builtin_res reg) :=
-  match r with
-  | BR id => do r <- find_var map id; ret (BR r)
-  | BR_none => ret BR_none
-  | _ => error (Errors.msg "RTLgen: bad builtin_res")
+Definition convert_builtin_res (map: mapping) (oty: option typ) (r: builtin_res ident) : mon (builtin_res reg) :=
+  match r, oty with
+  | BR id, _ => do r <- find_var map id; ret (BR r)
+  | BR_none, None => ret BR_none
+  | BR_none, Some _ => do r <- new_reg; ret (BR r)
+  | _, _ => error (Errors.msg "RTLgen: bad builtin_res")
   end.
 
 (** Translation of an expression.  [transl_expr map a rd nd]
@@ -598,7 +599,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       let al := exprlist_of_expr_list (params_of_builtin_args args) in
       do rargs <- alloc_regs map al;
       let args' := convert_builtin_args args rargs in
-      do res' <- convert_builtin_res map res;
+      do res' <- convert_builtin_res map (sig_res (ef_sig ef)) res;
       do n1 <- add_instr (Ibuiltin ef args' res' nd);
          transl_exprlist map al rargs n1
   | Sseq s1 s2 =>
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 559ab3a2..19f6f1f4 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -234,6 +234,7 @@ Proof.
   intros. inv H1; simpl.
 - eapply match_env_update_var; eauto.
 - auto.
+- eapply match_env_update_temp; eauto.
 Qed.
 
 (** Matching and [let]-bound variables. *)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 41b5016f..1e665002 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -814,7 +814,10 @@ Inductive tr_builtin_res: mapping -> builtin_res ident -> builtin_res reg -> Pro
       map.(map_vars)!id = Some r ->
       tr_builtin_res map (BR id) (BR r)
   | tr_builtin_res_none: forall map,
-      tr_builtin_res map BR_none BR_none.
+      tr_builtin_res map BR_none BR_none
+  | tr_builtin_res_fresh: forall map r,
+      ~reg_in_map map r ->
+      tr_builtin_res map BR_none (BR r).
 
 (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c],
   starting at node [ns], contains instructions that perform the Cminor
@@ -1214,14 +1217,17 @@ Proof.
 Qed.
 
 Lemma convert_builtin_res_charact:
-  forall map res s res' s' INCR
-    (TR: convert_builtin_res map res s = OK res' s' INCR)
+  forall map oty res s res' s' INCR
+    (TR: convert_builtin_res map oty res s = OK res' s' INCR)
     (WF: map_valid map s),
   tr_builtin_res map res res'.
 Proof.
-  destruct res; simpl; intros; monadInv TR. 
-- constructor.  unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
-- constructor.
+  destruct res; simpl; intros.
+- monadInv TR. constructor.  unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
+- destruct oty; monadInv TR.
++ constructor. eauto with rtlg. 
++ constructor.
+- monadInv TR.
 Qed.
 
 Lemma transl_stmt_charact:
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 6569bb4c..fbf57082 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -111,16 +111,16 @@ let pack_bitfields env sid ml =
           end
   in pack [] 0 ml
 
-let rec transf_members env id count = function
+let rec transf_struct_members env id count = function
   | [] -> []
   | m :: ms as ml ->
       if m.fld_bitfield = None then
-        m :: transf_members env id count ms
+        m :: transf_struct_members env id count ms
       else begin
         let (nbits, bitfields, ml') = pack_bitfields env id ml in
         if nbits = 0 then
           (* Lone zero-size bitfield: just ignore *)
-          transf_members env id count ml'
+          transf_struct_members env id count ml'
         else begin
           (* Create integer field of sufficient size for this bitfield group *)
           let carrier = sprintf "__bf%d" count in
@@ -143,14 +143,49 @@ let rec transf_members env id count = function
               end)
             bitfields;
           { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
-          :: transf_members env id (count + 1) ml'
+          :: transf_struct_members env id (count + 1) ml'
         end
       end
 
+let rec transf_union_members env id count = function
+    [] -> []
+  | m :: ms ->
+      (match m.fld_bitfield with
+      | None ->  m::transf_union_members env id count ms
+      | Some nbits ->
+          let carrier = sprintf "__bf%d" count in
+          let carrier_ikind = unsigned_ikind_for_carrier nbits in
+          let carrier_typ = TInt(carrier_ikind, []) in
+          let signed =
+            match unroll env m.fld_typ with
+            | TInt(ik, _) -> is_signed_ikind ik
+            | TEnum(eid, _) -> is_signed_enum_bitfield env id m.fld_name eid nbits
+            | _ -> assert false (* should never happen, checked in Elab *) in
+          let signed2 =
+            match unroll env (type_of_member env m) with
+            | TInt(ik, _) -> is_signed_ikind ik
+            | _ -> assert false (* should never happen, checked in Elab *) in
+          let pos' =
+            if !config.bitfields_msb_first
+            then sizeof_ikind carrier_ikind * 8 - nbits
+            else 0 in
+          let is_bool =
+            match unroll env m.fld_typ with
+            | TInt(IBool, _) -> true
+            | _ -> false in
+          Hashtbl.add bitfield_table
+            (id, m.fld_name)
+            {bf_carrier = carrier; bf_carrier_typ = carrier_typ;
+             bf_pos = pos'; bf_size = nbits;
+             bf_signed = signed; bf_signed_res = signed2;
+             bf_bool = is_bool};
+          { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
+          :: transf_struct_members env id (count + 1) ms)
+
 let transf_composite env su id attr ml =
   match su with
-  | Struct -> (attr, transf_members env id 1 ml)
-  | Union  -> (attr, ml)
+  | Struct -> (attr, transf_struct_members env id 1 ml)
+  | Union  -> (attr, transf_union_members env id 1 ml)
 
 (* Bitfield manipulation expressions *)
 
@@ -317,6 +352,7 @@ let rec is_bitfield_access env e =
   match e.edesc with
   | EUnop(Odot fieldname, e1) ->
       begin match unroll env e1.etyp with
+      | TUnion (id,_)
       | TStruct(id, _) ->
           (try Some(e1, Hashtbl.find bitfield_table (id, fieldname))
            with Not_found -> None)
diff --git a/test/c/aes.c b/test/c/aes.c
index abdaf6c3..88b3de4a 100644
--- a/test/c/aes.c
+++ b/test/c/aes.c
@@ -1423,7 +1423,7 @@ static void do_test(int keybits, u8 * key,
 static void do_bench(int nblocks)
 {
   u32 ckey[4 * (MAXNR + 1)];
-  u8 temp[16];
+  u8 temp[16] = "Plaintext";
   int nr;
 
   nr = rijndaelKeySetupEnc(ckey, (u8 *)"\x00\x01\x02\x03\x04\x05\x06\x07\x08\x09\x0A\x0B\x0C\x0D\x0E\x0F", 128);
diff --git a/test/regression/alias.c b/test/regression/alias.c
index a38e6dfd..9887ae2b 100644
--- a/test/regression/alias.c
+++ b/test/regression/alias.c
@@ -1,8 +1,8 @@
 /* Testing the alias analysis on ill-defined codes 
    where it should remain conservative. */
 
-typedef unsigned int uintptr_t;
-typedef signed int ptrdiff_t;
+#include <stddef.h>
+#include <stdint.h>
 
 /* For testing with GCC */
 #define NOINLINE __attribute__((noinline))
diff --git a/test/regression/builtins-arm.c b/test/regression/builtins-arm.c
index 91a8e890..643c8f1a 100644
--- a/test/regression/builtins-arm.c
+++ b/test/regression/builtins-arm.c
@@ -23,7 +23,10 @@ int main(int argc, char ** argv)
   y = 0;
   __builtin_write32_reversed(&y, 0x12345678);
   printf ("CSE write_32_rev: %s\n", y == 0x78563412 ? "ok" : "ERROR");
-
+  /* Make sure that ignoring the result of a builtin
+     doesn't cause an internal error */
+  (void) __builtin_bswap(x);
+  (void) __builtin_fsqrt(a);
   return 0;
 }
 
diff --git a/test/regression/builtins-ia32.c b/test/regression/builtins-ia32.c
index 10426209..558c3153 100644
--- a/test/regression/builtins-ia32.c
+++ b/test/regression/builtins-ia32.c
@@ -36,7 +36,10 @@ int main(int argc, char ** argv)
   y = 0;
   __builtin_write32_reversed(&y, 0x12345678);
   printf ("CSE write_32_rev: %s\n", y == 0x78563412 ? "ok" : "ERROR");
-
+  /* Make sure that ignoring the result of a builtin
+     doesn't cause an internal error */
+  (void) __builtin_bswap(x);
+  (void) __builtin_fsqrt(a);
   return 0;
 }
 
diff --git a/test/regression/builtins-powerpc.c b/test/regression/builtins-powerpc.c
index acffa435..90030737 100644
--- a/test/regression/builtins-powerpc.c
+++ b/test/regression/builtins-powerpc.c
@@ -50,7 +50,10 @@ int main(int argc, char ** argv)
   y = 0;
   __builtin_write32_reversed(&y, 0x12345678);
   printf ("CSE write_32_rev: %s\n", y == 0x78563412 ? "ok" : "ERROR");
-
+  /* Make sure that ignoring the result of a builtin
+     doesn't cause an internal error */
+  (void) __builtin_bswap(x);
+  (void) __builtin_fsqrt(a);
   return 0;
 }