diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-17 19:08:51 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-17 19:08:51 +0200 |
commit | 66f3da28ee1e75732d07dd7ba851a0106513c9da (patch) | |
tree | ce59eccdf0052f1835f5f5c0539c7a6bc3bcaef1 | |
parent | fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49 (diff) | |
parent | b24913a4ad1014b7da42bdb1deb8f3cc05b0ed8d (diff) | |
download | compcert-66f3da28ee1e75732d07dd7ba851a0106513c9da.tar.gz compcert-66f3da28ee1e75732d07dd7ba851a0106513c9da.zip |
Merge branch 'master' into atomic-builtins
-rw-r--r-- | backend/RTL.v | 3 | ||||
-rw-r--r-- | backend/RTLgen.v | 13 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 1 | ||||
-rw-r--r-- | backend/RTLgenspec.v | 18 | ||||
-rw-r--r-- | cparser/Bitfields.ml | 48 | ||||
-rw-r--r-- | test/c/aes.c | 2 | ||||
-rw-r--r-- | test/regression/alias.c | 4 | ||||
-rw-r--r-- | test/regression/builtins-arm.c | 5 | ||||
-rw-r--r-- | test/regression/builtins-ia32.c | 5 | ||||
-rw-r--r-- | test/regression/builtins-powerpc.c | 5 |
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; } |