diff options
-rw-r--r-- | backend/Constprop.v | 6 | ||||
-rw-r--r-- | backend/Constpropproof.v | 6 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 5 | ||||
-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-- | cfrontend/C2C.ml | 74 | ||||
-rw-r--r-- | cfrontend/Ctypes.v | 6 | ||||
-rw-r--r-- | cparser/Bitfields.ml | 48 | ||||
-rw-r--r-- | cparser/Elab.ml | 2 | ||||
-rw-r--r-- | cparser/Unblock.ml | 164 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml | 8 | ||||
-rw-r--r-- | debug/DwarfTypes.mli | 1 | ||||
-rw-r--r-- | debug/DwarfUtil.ml | 1 | ||||
-rw-r--r-- | powerpc/Asm.v | 10 | ||||
-rw-r--r-- | powerpc/AsmToJSON.ml | 6 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 100 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 2 | ||||
-rw-r--r-- | powerpc/CBuiltins.ml | 12 | ||||
-rw-r--r-- | powerpc/Machregs.v | 6 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 6 | ||||
-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 |
27 files changed, 342 insertions, 177 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index cd844d30..8f4cb76d 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -144,9 +144,9 @@ Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) := | a :: al => let a' := builtin_arg_reduction ae a in let al' := a :: debug_strength_reduction ae al in - match a' with - | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al' - | _ => al' + match a, a' with + | BA _, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => a' :: al' + | _, _ => al' end end. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index d9005f5e..eafefed5 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -243,7 +243,11 @@ Proof. induction 2; simpl. - exists (@nil val); constructor. - destruct IHlist_forall2 as (vl' & A). - destruct (builtin_arg_reduction ae a1); repeat (eauto; econstructor). + assert (eval_builtin_args ge (fun r => rs#r) sp m + (a1 :: debug_strength_reduction ae al) (b1 :: vl')) + by (constructor; eauto). + destruct a1; try (econstructor; eassumption). + destruct (builtin_arg_reduction ae (BA x)); repeat (eauto; econstructor). Qed. Lemma builtin_strength_reduction_correct: diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 2daa2d56..ed0fe524 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -266,6 +266,8 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args = args in match kind with | 1 -> (* line number *) + fprintf oc "%s debug: current scopes%a\n" + comment print_debug_args args; if Str.string_match re_file_line txt 0 then print_line oc (Str.matched_group 1 txt) (int_of_string (Str.matched_group 2 txt)) @@ -280,6 +282,9 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args = | 5 -> (* local variable preallocated in stack *) fprintf oc "%s debug: %s resides at%a\n" comment txt print_debug_args args + | 6 -> (* declaration of a local variable *) + fprintf oc "%s debug: %s declared in scope%a\n" + comment txt print_debug_args args | _ -> () 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/cfrontend/C2C.ml b/cfrontend/C2C.ml index b7012ef9..dd55e60f 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -746,6 +746,22 @@ let rec convertExpr env e = | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero + | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) -> + let (kind, args1) = + match args with + | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1) + | _ -> error "ill_formed __builtin_debug"; (0L, args) in + let (text, args2) = + match args1 with + | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2) + | {edesc = C.EVar id} :: args2 -> (id.name, args2) + | _ -> error "ill_formed __builtin_debug"; ("", args1) in + let targs2 = convertTypArgs env [] args2 in + Ebuiltin( + EF_debug(P.of_int64 kind, intern_string text, + typlist_of_typelist targs2), + targs2, convertExprList env args2, convertTyp env e.etyp) + | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> @@ -927,16 +943,6 @@ let rec contains_case s = (** Annotations for line numbers *) -let add_lineno prev_loc this_loc s = - if !Clflags.option_g && prev_loc <> this_loc && this_loc <> Cutil.no_loc - then begin - let txt = sprintf "#line:%s:%d" (fst this_loc) (snd this_loc) in - Ssequence(Sdo(Ebuiltin(EF_debug(P.one, intern_string txt, []), - Tnil, Enil, Tvoid)), - s) - end else - s - (** Statements *) let swrap = function @@ -944,36 +950,31 @@ let swrap = function | Errors.Error msg -> error ("retyping error: " ^ string_of_errmsg msg); Sskip -let rec convertStmt ploc env s = +let rec convertStmt env s = updateLoc s.sloc; match s.sdesc with | C.Sskip -> Sskip | C.Sdo e -> - add_lineno ploc s.sloc (swrap (Ctyping.sdo (convertExpr env e))) + swrap (Ctyping.sdo (convertExpr env e)) | C.Sseq(s1, s2) -> - let s1' = convertStmt ploc env s1 in - let s2' = convertStmt s1.sloc env s2 in + let s1' = convertStmt env s1 in + let s2' = convertStmt env s2 in Ssequence(s1', s2') | C.Sif(e, s1, s2) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sifthenelse te - (convertStmt s.sloc env s1) (convertStmt s.sloc env s2))) + swrap (Ctyping.sifthenelse te (convertStmt env s1) (convertStmt env s2)) | C.Swhile(e, s1) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.swhile te (convertStmt s.sloc env s1))) + swrap (Ctyping.swhile te (convertStmt env s1)) | C.Sdowhile(s1, e) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sdowhile te (convertStmt s.sloc env s1))) + swrap (Ctyping.sdowhile te (convertStmt env s1)) | C.Sfor(s1, e, s2, s3) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sfor - (convertStmt s.sloc env s1) te - (convertStmt s.sloc env s2) (convertStmt s.sloc env s3))) + swrap (Ctyping.sfor + (convertStmt env s1) te + (convertStmt env s2) (convertStmt env s3)) | C.Sbreak -> Sbreak | C.Scontinue -> @@ -986,22 +987,20 @@ let rec convertStmt ploc env s = contains_case init end; let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sswitch te - (convertSwitch s.sloc env (is_longlong env e.etyp) cases))) + swrap (Ctyping.sswitch te + (convertSwitch env (is_longlong env e.etyp) cases)) | C.Slabeled(C.Slabel lbl, s1) -> - add_lineno ploc s.sloc - (Slabel(intern_string lbl, convertStmt s.sloc env s1)) + Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> unsupported "'case' outside of 'switch'"; Sskip | C.Slabeled(C.Sdefault, _) -> unsupported "'default' outside of 'switch'"; Sskip | C.Sgoto lbl -> - add_lineno ploc s.sloc (Sgoto(intern_string lbl)) + Sgoto(intern_string lbl) | C.Sreturn None -> - add_lineno ploc s.sloc (Sreturn None) + Sreturn None | C.Sreturn(Some e) -> - add_lineno ploc s.sloc (Sreturn(Some(convertExpr env e))) + Sreturn(Some(convertExpr env e)) | C.Sblock _ -> unsupported "nested blocks"; Sskip | C.Sdecl _ -> @@ -1009,10 +1008,9 @@ let rec convertStmt ploc env s = | C.Sasm(attrs, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then unsupported "inline 'asm' statement (consider adding option -finline-asm)"; - add_lineno ploc s.sloc - (Sdo (convertAsm s.sloc env txt outputs inputs clobber)) + Sdo (convertAsm s.sloc env txt outputs inputs clobber) -and convertSwitch ploc env is_64 = function +and convertSwitch env is_64 = function | [] -> LSnil | (lbl, s) :: rem -> @@ -1029,7 +1027,7 @@ and convertSwitch ploc env is_64 = function then Z.of_uint64 v else Z.of_uint32 (Int64.to_int32 v)) in - LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env is_64 rem) + LScons(lbl', convertStmt env s, convertSwitch env is_64 rem) (** Function definitions *) @@ -1057,7 +1055,7 @@ let convertFundef loc env fd = Debug.atom_local_variable id id'; (id', convertTyp env ty)) fd.fd_locals in - let body' = convertStmt loc env fd.fd_body in + let body' = convertStmt env fd.fd_body in let id' = intern_string fd.fd_name.name in Debug.atom_function fd.fd_name id'; Hashtbl.add decl_atom id' diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index a555f792..1f55da7f 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -802,13 +802,13 @@ Program Definition composite_of_def Next Obligation. apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. apply align_le; apply alignof_composite_pos. -Qed. +Defined. Next Obligation. apply align_attr_two_p. apply alignof_composite_two_p. -Qed. +Defined. Next Obligation. apply align_divides. apply alignof_composite_pos. -Qed. +Defined. (** The composite environment for a program is obtained by entering its composite definitions in sequence. The definitions are assumed diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index cae56f00..d064f4b1 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 @@ -144,14 +144,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 *) @@ -318,6 +353,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/cparser/Elab.ml b/cparser/Elab.ml index e802085d..021dc512 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1839,7 +1839,7 @@ let enter_or_refine_ident local loc env s sto ty = let enter_decdefs local loc env sto dl = (* Sanity checks on storage class *) if sto = Storage_register && not local then - error loc "'register' on global declaration"; + fatal_error loc "'register' on global declaration"; if sto <> Storage_default && dl = [] then warning loc "Storage class specifier on empty declaration"; let rec enter_decdef (decls, env) (s, ty, init) = diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 91f50552..b5f945d4 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -177,74 +177,173 @@ and expand_init islocal env i = in expand i +(* Insertion of debug annotation, for -g mode *) + +let debug_id = Env.fresh_ident "__builtin_debug" +let debug_ty = + TFun(TVoid [], Some [Env.fresh_ident "kind", TInt(IInt, [])], true, []) + +let debug_annot kind args = + { sloc = no_loc; + sdesc = Sdo { + etyp = TVoid []; + edesc = ECall({edesc = EVar debug_id; etyp = debug_ty}, + intconst kind IInt :: args) + } + } + +let string_const str = + let c = CStr str in { edesc = EConst c; etyp = type_of_constant c } + +let integer_const n = + intconst (Int64.of_int n) IInt + +(* Line number annotation: + __builtin_debug(1, "#line:filename:lineno", scope1, ..., scopeN) *) +(* TODO: consider + __builtin_debug(1, "filename", lineno, scope1, ..., scopeN) + instead. *) + +let debug_lineno ctx (filename, lineno) = + debug_annot 1L + (string_const (Printf.sprintf "#line:%s:%d" filename lineno) :: + List.rev_map integer_const ctx) + +let add_lineno ctx prev_loc this_loc s = + if !Clflags.option_g && this_loc <> prev_loc && this_loc <> no_loc + then sseq no_loc (debug_lineno ctx this_loc) s + else s + +(* Variable declaration annotation: + __builtin_debug(6, var, scope) *) + +let debug_var_decl ctx id ty = + let scope = match ctx with [] -> 0 | sc :: _ -> sc in + debug_annot 6L + [ {edesc = EVar id; etyp = ty}; integer_const scope ] + +let add_var_decl ctx id ty s = + if !Clflags.option_g + then sseq no_loc (debug_var_decl ctx id ty) s + else s + +let add_param_decls params body = + if !Clflags.option_g then + List.fold_right + (fun (id, ty) s -> sseq no_loc (debug_var_decl [] id ty) s) + params body + else body + +(* Generate fresh scope identifiers, for blocks that contain at least + one declaration *) + +let block_contains_decl sl = + List.exists + (function {sdesc = Sdecl _} -> true | _ -> false) + sl + +let next_scope_id = ref 0 + +let new_scope_id () = + incr next_scope_id; !next_scope_id + (* Process a block-scoped variable declaration. The variable is entered in [local_variables]. The initializer, if any, is converted into assignments and prepended to [k]. *) -let process_decl loc env (sto, id, ty, optinit) k = +let process_decl loc env ctx (sto, id, ty, optinit) k = let ty' = remove_const env ty in local_variables := (sto, id, ty', None) :: !local_variables; - match optinit with - | None -> k - | Some init -> - let init' = expand_init true env init in - let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in - add_inits_stmt loc l k + add_var_decl ctx id ty + (match optinit with + | None -> + k + | Some init -> + let init' = expand_init true env init in + let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in + add_inits_stmt loc l k) (* Simplification of blocks within a statement *) -let rec unblock_stmt env s = +let rec unblock_stmt env ctx ploc s = match s.sdesc with | Sskip -> s | Sdo e -> - {s with sdesc = Sdo(expand_expr true env e)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sdo(expand_expr true env e)} | Sseq(s1, s2) -> - {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)} + {s with sdesc = Sseq(unblock_stmt env ctx ploc s1, + unblock_stmt env ctx s1.sloc s2)} | Sif(e, s1, s2) -> - {s with sdesc = Sif(expand_expr true env e, - unblock_stmt env s1, unblock_stmt env s2)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sif(expand_expr true env e, + unblock_stmt env ctx s.sloc s1, + unblock_stmt env ctx s.sloc s2)} | Swhile(e, s1) -> - {s with sdesc = Swhile(expand_expr true env e, unblock_stmt env s1)} + add_lineno ctx ploc s.sloc + {s with sdesc = Swhile(expand_expr true env e, + unblock_stmt env ctx s.sloc s1)} | Sdowhile(s1, e) -> - {s with sdesc = Sdowhile(unblock_stmt env s1, expand_expr true env e)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sdowhile(unblock_stmt env ctx s.sloc s1, + expand_expr true env e)} | Sfor(s1, e, s2, s3) -> - {s with sdesc = Sfor(unblock_stmt env s1, - expand_expr true env e, - unblock_stmt env s2, - unblock_stmt env s3)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sfor(unblock_stmt env ctx s.sloc s1, + expand_expr true env e, + unblock_stmt env ctx s.sloc s2, + unblock_stmt env ctx s.sloc s3)} | Sbreak -> s | Scontinue -> s | Sswitch(e, s1) -> - {s with sdesc = Sswitch(expand_expr true env e, unblock_stmt env s1)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sswitch(expand_expr true env e, + unblock_stmt env ctx s.sloc s1)} | Slabeled(lbl, s1) -> - {s with sdesc = Slabeled(lbl, unblock_stmt env s1)} - | Sgoto lbl -> s - | Sreturn None -> s + add_lineno ctx ploc s.sloc + {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)} + | Sgoto lbl -> + add_lineno ctx ploc s.sloc s + | Sreturn None -> + add_lineno ctx ploc s.sloc s | Sreturn (Some e) -> - {s with sdesc = Sreturn(Some (expand_expr true env e))} - | Sblock sl -> unblock_block env sl - | Sdecl d -> assert false + add_lineno ctx ploc s.sloc + {s with sdesc = Sreturn(Some (expand_expr true env e))} + | Sblock sl -> + let ctx' = + if block_contains_decl sl + then new_scope_id () :: ctx + else ctx in + unblock_block env ctx' ploc sl + | Sdecl d -> + assert false | Sasm(attr, template, outputs, inputs, clob) -> let expand_asm_operand (lbl, cstr, e) = (lbl, cstr, expand_expr true env e) in - {s with sdesc = Sasm(attr, template, - List.map expand_asm_operand outputs, - List.map expand_asm_operand inputs, clob)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sasm(attr, template, + List.map expand_asm_operand outputs, + List.map expand_asm_operand inputs, clob)} -and unblock_block env = function +and unblock_block env ctx ploc = function | [] -> sskip | {sdesc = Sdecl d; sloc = loc} :: sl -> - process_decl loc env d (unblock_block env sl) + add_lineno ctx ploc loc + (process_decl loc env ctx d + (unblock_block env ctx loc sl)) | s :: sl -> - sseq s.sloc (unblock_stmt env s) (unblock_block env sl) + sseq s.sloc (unblock_stmt env ctx ploc s) + (unblock_block env ctx s.sloc sl) (* Simplification of blocks and compound literals within a function *) let unblock_fundef env f = local_variables := []; - let body = unblock_stmt env f.fd_body in + next_scope_id := 0; + let body = + add_param_decls f.fd_params (unblock_stmt env [] no_loc f.fd_body) in let decls = !local_variables in local_variables := []; { f with fd_locals = f.fd_locals @ decls; fd_body = body } @@ -299,4 +398,5 @@ let rec unblock_glob env accu = function (* Entry point *) let program p = + {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} :: unblock_glob (Builtins.environment()) [] p diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index a0b16463..5e58e365 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -58,6 +58,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let add_byte_size = add_abbr_entry (0xb,byte_size_type_abbr) + let add_member_size = add_abbr_entry (0xb,member_size_abbr) + let add_high_pc = add_abbr_entry (0x12,high_pc_type_abbr) let add_low_pc = add_abbr_entry (0x11,low_pc_type_abbr) @@ -153,7 +155,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): | DW_TAG_structure_type e -> prologue 0x13; add_attr_some e.structure_file_loc add_file_loc; - add_attr_some e.structure_byte_size add_byte_size; + add_attr_some e.structure_byte_size add_member_size; add_attr_some e.structure_declaration add_declaration; add_attr_some e.structure_name add_name | DW_TAG_subprogram e -> @@ -184,7 +186,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): | DW_TAG_union_type e -> prologue 0x17; add_attr_some e.union_file_loc add_file_loc; - add_attr_some e.union_byte_size add_byte_size; + add_attr_some e.union_byte_size add_member_size; add_attr_some e.union_declaration add_declaration; add_attr_some e.union_name add_name | DW_TAG_unspecified_parameter e -> @@ -246,7 +248,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): fprintf oc " .uleb128 %d\n" id; output_string oc s; fprintf oc " .uleb128 0\n"; - fprintf oc " .uleb128 0\n") abbrevs; + fprintf oc " .uleb128 0\n\n") abbrevs; fprintf oc " .sleb128 0\n" let debug_start_addr = ref (-1) diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index eb7d4060..b5be3121 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -242,6 +242,7 @@ module type DWARF_ABBREVS = val name_type_abbr: int val encoding_type_abbr: int val byte_size_type_abbr: int + val member_size_abbr: int val high_pc_type_abbr: int val low_pc_type_abbr: int val stmt_list_type_abbr: int diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml index d5e72adb..4cd838b6 100644 --- a/debug/DwarfUtil.ml +++ b/debug/DwarfUtil.ml @@ -85,6 +85,7 @@ module DefaultAbbrevs = let name_type_abbr = dw_form_string let encoding_type_abbr = dw_form_data1 let byte_size_type_abbr = dw_form_data1 + let member_size_abbr = dw_form_udata let high_pc_type_abbr = dw_form_addr let low_pc_type_abbr = dw_form_addr let stmt_list_type_abbr = dw_form_data4 diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 863ed6a1..3c7bdd15 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -142,7 +142,7 @@ Inductive instruction : Type := | Paddic: ireg -> ireg -> constant -> instruction (**r add immediate and set carry *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) | Paddze: ireg -> ireg -> instruction (**r add carry *) - | Pallocframe: Z -> int -> instruction (**r allocate new stack frame (pseudo) *) + | Pallocframe: Z -> int -> int -> instruction (**r allocate new stack frame (pseudo) *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) @@ -157,6 +157,7 @@ Inductive instruction : Type := | Pblr: instruction (**r branch to contents of register LR *) | Pbt: crbit -> label -> instruction (**r branch if true *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table (pseudo) *) + | Pcmpb: ireg -> ireg -> ireg -> instruction (**r compare bytes *) | Pcmplw: ireg -> ireg -> instruction (**r unsigned integer comparison *) | Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *) | Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *) @@ -206,6 +207,7 @@ Inductive instruction : Type := | Pfrsqrte: freg -> freg -> instruction (**r approximate reciprocal of square root *) | Pfres: freg -> freg -> instruction (**r approximate inverse *) | Pfsel: freg -> freg -> freg -> freg -> instruction (**r FP conditional move *) + | Pisel: ireg -> ireg -> ireg -> crbit -> instruction (**r integer select *) | Pisync: instruction (**r ISYNC barrier *) | Picbi: ireg -> ireg -> instruction (**r instruction cache invalidate *) | Picbtls: int -> ireg -> ireg -> instruction (**r instruction cache block touch and lock set *) @@ -323,7 +325,7 @@ lbl: .double floatcst lfd rdst, 0(r1) addi r1, r1, 8 >> -- [Pallocframe sz ofs]: in the formal semantics, this pseudo-instruction +- [Pallocframe sz ofs retofs]: in the formal semantics, this pseudo-instruction allocates a memory block with bounds [0] and [sz], stores the value of register [r1] (the stack pointer, by convention) at offset [ofs] in this block, and sets [r1] to a pointer to the bottom of this @@ -622,7 +624,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Paddze rd r1 => Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY) #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m - | Pallocframe sz ofs => + | Pallocframe sz ofs _ => let (m1, stk) := Mem.alloc m 0 sz in let sp := Vptr stk Int.zero in match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with @@ -871,6 +873,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** The following instructions and directives are not generated directly by [Asmgen], so we do not model them. *) | Pbdnz _ + | Pcmpb _ _ _ | Pcntlzw _ _ | Pcreqv _ _ _ | Pcrxor _ _ _ @@ -891,6 +894,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfrsqrte _ _ | Pfres _ _ | Pfsel _ _ _ _ + | Pisel _ _ _ _ | Plwarx _ _ _ | Plwbrx _ _ _ | Picbi _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 5f875ebf..a7e66701 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -152,7 +152,7 @@ let p_instruction oc ic = | Paddic (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Paddis (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddis\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Paddze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Paddze\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 - | Pallocframe (c,i) -> assert false(* Should not occur *) + | Pallocframe (c,i,r) -> assert false(* Should not occur *) | Pand_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pand_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pandc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pandc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c @@ -167,6 +167,7 @@ let p_instruction oc ic = | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}" | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l | Pbtbl (i,lb) -> fprintf oc "{\"Instruction Name\":\"Pbtl\",\"Args\":[%a%a]}" p_ireg i (p_list_cont p_label) lb + | Pcmpb (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pcmpb\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pcmplw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmplw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pcmplwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmplwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c | Pcmpw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmpw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 @@ -216,6 +217,7 @@ let p_instruction oc ic = | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pisel (ir1,ir2,ir3,cr) -> fprintf oc "{\"Instruction Name\":\"Pisel\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 p_crbit cr | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Picbtls (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2 | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" @@ -286,7 +288,7 @@ let p_instruction oc ic = | Pstwx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstwux (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwux\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwc_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwcx_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psubfc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psubfe (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psubfze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 3e57cdbf..b9fe1d7f 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -276,6 +276,9 @@ let expand_builtin_vstore chunk args = assert false (* Handling of varargs *) +let linkregister_offset = ref Int.zero + +let retaddr_offset = ref Int.zero let current_function_stacksize = ref 0l @@ -324,56 +327,6 @@ let expand_builtin_va_start r = let expand_int64_arith conflict rl fn = if conflict then (fn GPR0; emit (Pmr(rl, GPR0))) else fn rl -(* Handling of cache instructions *) - -(* Auxiliary function to generate address for the cache function *) -let expand_builtin_cache_common addr f = - let add = match addr with - | BA (IR a1) -> a1 - | BA_addrstack ofs -> - emit_addimm GPR11 GPR1 ofs; - GPR11 - | BA_addrglobal(id, ofs) -> - if symbol_is_small_data id ofs then begin - emit (Paddi (GPR11, GPR0, Csymbol_sda(id, ofs))); - GPR11 - end else if symbol_is_rel_data id ofs then begin - emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs))); - emit (Paddi(GPR11, GPR11, Csymbol_rel_low(id, ofs))); - GPR11 - end else begin - emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs))); - emit (Paddi (GPR11, GPR11, Csymbol_low(id, ofs))); - GPR11 - end - | _ -> raise (Error "Argument is not an address") in - f add - -let expand_builtin_prefetch addr rw loc = - if not ((loc >= _0) && (loc <= _2)) then - raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 2"); - let emit_prefetch_instr addr = - if Int.eq rw _0 then begin - emit (Pdcbt (loc,GPR0,addr)); - end else if Int.eq rw _1 then begin - emit (Pdcbtst (loc,GPR0,addr)); - end else - raise (Error "the second argument of __builtin_prefetch must be either 0 or 1") - in - expand_builtin_cache_common addr emit_prefetch_instr - -let expand_builtin_dcbtls addr loc = - if not ((loc == _0) || (loc = _2)) then - raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2"); - let emit_inst addr = emit (Pdcbtls (loc,GPR0,addr)) in - expand_builtin_cache_common addr emit_inst - -let expand_builtin_icbtls addr loc = - if not ((loc == _0) || (loc = _2)) then - raise (Error "the second argument of __builtin_icbtls must be a constant between 0 and 2"); - let emit_inst addr = emit (Picbtls (loc,GPR0,addr)) in - expand_builtin_cache_common addr emit_inst - (* Handling of compiler-inlined builtins *) let expand_builtin_inline name args res = @@ -386,6 +339,8 @@ let expand_builtin_inline name args res = emit (Pmulhwu(res, a1, a2)) | "__builtin_clz", [BA(IR a1)], BR(IR res) -> emit (Pcntlzw(res, a1)) + | "__builtin_cmpb", [BA(IR a1); BA(IR a2)], BR(IR res) -> + emit (Pcmpb (res,a1,a2)) | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> emit (Pstwu(a1, Cint _m8, GPR1)); emit (Pcfi_adjust _8); @@ -468,7 +423,7 @@ let expand_builtin_inline name args res = emit (Plwsync) | "__builtin_mbar", [BA_int mo], _ -> if not (mo = _0 || mo = _1) then - raise (Error "the argument of __builtin_mbar must be either 0 or 1"); + raise (Error "the argument of __builtin_mbar must be 0 or 1"); emit (Pmbar mo) | "__builin_mbar",_, _ -> raise (Error "the argument of __builtin_mbar must be a constant"); @@ -484,16 +439,27 @@ let expand_builtin_inline name args res = emit (Pdcbi (GPR0,a1)) | "__builtin_icbi", [BA(IR a1)],_ -> emit (Picbi(GPR0,a1)) - | "__builtin_dcbtls", [a; BA_int loc],_ -> - expand_builtin_dcbtls a loc + | "__builtin_dcbtls", [BA (IR a1); BA_int loc],_ -> + if not ((Int.eq loc _0) || (Int.eq loc _2)) then + raise (Error "the second argument of __builtin_dcbtls must be 0 or 2"); + emit (Pdcbtls (loc,GPR0,a1)) | "__builtin_dcbtls",_,_ -> raise (Error "the second argument of __builtin_dcbtls must be a constant") - | "__builtin_icbtls", [a; BA_int loc],_ -> - expand_builtin_icbtls a loc + | "__builtin_icbtls", [BA (IR a1); BA_int loc],_ -> + if not ((Int.eq loc _0) || (Int.eq loc _2)) then + raise (Error "the second argument of __builtin_icbtls must be 0 or 2"); + emit (Picbtls (loc,GPR0,a1)) | "__builtin_icbtls",_,_ -> raise (Error "the second argument of __builtin_icbtls must be a constant") - | "__builtin_prefetch" , [a1 ;BA_int rw; BA_int loc],_ -> - expand_builtin_prefetch a1 rw loc + | "__builtin_prefetch" , [BA (IR a1) ;BA_int rw; BA_int loc],_ -> + if not (Int.ltu loc _4) then + raise (Error "the last argument of __builtin_prefetch must be 0, 1 or 2"); + if Int.eq rw _0 then begin + emit (Pdcbt (loc,GPR0,a1)); + end else if Int.eq rw _1 then begin + emit (Pdcbtst (loc,GPR0,a1)); + end else + raise (Error "the second argument of __builtin_prefetch must be 0 or 1") | "__builtin_prefetch" ,_,_ -> raise (Error "the second and third argument of __builtin_prefetch must be a constant") | "__builtin_dcbz",[BA (IR a1)],_ -> @@ -507,6 +473,20 @@ let expand_builtin_inline name args res = emit (Pmtspr(n, a1)) | "__builtin_set_spr", _, _ -> raise (Error "the first argument of __builtin_set_spr must be a constant") + (* Frame and return address *) + | "__builtin_call_frame", _,BR (IR res) -> + let sz = !current_function_stacksize + and ofs = !linkregister_offset in + if sz < 0x8000l then + emit (Paddi(res, GPR1, Cint(coqint_of_camlint sz))) + else + emit (Plwz(res, Cint ofs, GPR1)) + | "__builtin_return_address",_,BR (IR res) -> + emit (Plwz (res, Cint! retaddr_offset,GPR1)) + (* isel *) + | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> + emit (Pcmpwi (a1,Cint (Int.zero))); + emit (Pisel (res,a3,a2,CRbit_2)) (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -534,7 +514,7 @@ let num_crbit = function let expand_instruction instr = match instr with - | Pallocframe(sz, ofs) -> + | Pallocframe(sz, ofs,retofs) -> let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in let sz = camlint_of_coqint sz in assert (ofs = Int.zero); @@ -553,7 +533,9 @@ let expand_instruction instr = {sig_args = []; sig_res = None; sig_cc = cc_default})); emit (Pmtlr GPR0) end; - current_function_stacksize := sz + current_function_stacksize := sz; + linkregister_offset := ofs; + retaddr_offset := retofs | Pbctr sg | Pbctrl sg | Pbl(_, sg) | Pbs(_, sg) -> set_cr6 sg; emit instr diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 541fe7c6..db3b7028 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -711,7 +711,7 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo Definition transl_function (f: Mach.function) := do c <- transl_code' f f.(Mach.fn_code) false; OK (mkfunction f.(Mach.fn_sig) - (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: + (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) f.(fn_retaddr_ofs) :: Pmflr GPR0 :: Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pcfi_rel_offset f.(fn_retaddr_ofs) :: c)). diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index e18fdb2d..1bb8c6f7 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -36,6 +36,8 @@ let builtins = { (TInt(IUInt, []), [TInt(IUInt, [])], false); "__builtin_bswap16", (TInt(IUShort, []), [TInt(IUShort, [])], false); + "__builtin_cmpb", + (TInt (IUInt, []), [TInt(IUInt, []);TInt(IUInt, [])], false); (* Float arithmetic *) "__builtin_fmadd", (TFloat(FDouble, []), @@ -108,7 +110,15 @@ let builtins = { "__builtin_get_spr", (TInt(IUInt, []), [TInt(IInt, [])], false); "__builtin_set_spr", - (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false) + (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false); + (* Frame and return address *) + "__builtin_call_frame", + (TPtr (TVoid [],[]),[],false); + "__builtin_return_address", + (TPtr (TVoid [],[]),[],false); + (* isel *) + "__builtin_isel", + (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false) ] } diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 402f07d1..a2017dca 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -217,9 +217,9 @@ Definition builtin_constraints (ef: external_function) : | EF_builtin id sg => if ident_eq id builtin_get_spr then OK_const :: nil else if ident_eq id builtin_set_spr then OK_const :: OK_default :: nil - else if ident_eq id builtin_prefetch then OK_addrany :: OK_const :: OK_const :: nil - else if ident_eq id builtin_dcbtls then OK_addrany::OK_const::nil - else if ident_eq id builtin_icbtls then OK_addrany::OK_const::nil + else if ident_eq id builtin_prefetch then OK_default :: OK_const :: OK_const :: nil + else if ident_eq id builtin_dcbtls then OK_default::OK_const::nil + else if ident_eq id builtin_icbtls then OK_default::OK_const::nil else if ident_eq id builtin_mbar then OK_const::nil else nil | EF_vload _ => OK_addrany :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index c126f641..58117ee7 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -384,7 +384,7 @@ module Target (System : SYSTEM):TARGET = fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c | Paddze(r1, r2) -> fprintf oc " addze %a, %a\n" ireg r1 ireg r2 - | Pallocframe(sz, ofs) -> + | Pallocframe(sz, ofs, _) -> assert false | Pand_(r1, r2, r3) -> fprintf oc " and. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 @@ -443,6 +443,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " bctr\n"; jumptables := (lbl, tbl) :: !jumptables; fprintf oc "%s end pseudoinstr btbl\n" comment + | Pcmpb (r1, r2, r3) -> + fprintf oc " cmpb %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pcmplw(r1, r2) -> fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 | Pcmplwi(r1, c) -> @@ -537,6 +539,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fres %a, %a\n" freg r1 freg r2 | Pfsel(r1, r2, r3, r4) -> fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pisel (r1,r2,r3,cr) -> + fprintf oc " isel %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 crbit cr | Picbi (r1,r2) -> fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 | Picbtls (n,r1,r2) -> 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; } |