JIRA VER-881: avoid complex call lvals.
This scans for statement-level function calls which will have complex lvalue translations, either because their lvalues are compound expressions or because their function return type will be promoted to be stored. It treats them like expression-level function calls, with an additional call statement added (saving to a ret_ variable) and the complex lvalue step treated like an assignment.
This commit is contained in:
parent
f0795805d1
commit
f35caa8dca
|
@ -1608,6 +1608,13 @@ in
|
|||
mod3 = []}}
|
||||
end
|
||||
|
||||
fun treat_as_emb_fcall env (NONE,fn_e,args) = false
|
||||
| treat_as_emb_fcall env (SOME lv,fn_e,args) = let
|
||||
val (callee, (rettyp, _)) = fndes_callinfo env fn_e
|
||||
val lvtyp = cse_typing env lv
|
||||
val lv_plain = case enode lv of Var _ => true | _ => false
|
||||
in not lv_plain orelse lvtyp <> rettyp end
|
||||
|
||||
fun process_blockitem fname e bi = let
|
||||
in
|
||||
case bi of
|
||||
|
@ -1711,7 +1718,12 @@ in
|
|||
in
|
||||
(prechaos grs [stmt], e)
|
||||
end
|
||||
| AssignFnCall(eopt,fn_e,args) => let
|
||||
| AssignFnCall(eopt,fn_e,args) => if treat_as_emb_fcall e (eopt,fn_e,args)
|
||||
then let
|
||||
val lv = case eopt of SOME lv => lv
|
||||
| NONE => raise Fail "Trying to embed fcall without lval."
|
||||
in pst e (w (Assign(lv,ebogwrap (EFnCall(fn_e,args))))) end
|
||||
else let
|
||||
val (callee, _) = fndes_callinfo e fn_e
|
||||
(* the arguments need to be considered as being part of one big
|
||||
expression (rather than independently) in order for the
|
||||
|
|
|
@ -393,6 +393,24 @@ in
|
|||
app (print_lines o lines_serial o serial_defn) ast
|
||||
end
|
||||
|
||||
fun adjusted_complex_fncalls cse ast = let
|
||||
open Absyn_Serial
|
||||
|
||||
fun is_adjusted s = case snode s of
|
||||
(Assign(_,e)) => (case enode e of EFnCall _ => true | _ => false)
|
||||
| _ => false
|
||||
fun note_adjusteds s = if is_adjusted s
|
||||
then print ("adjusted fncall at: " ^
|
||||
SourcePos.toString (sleft s) ^ " " ^
|
||||
SourcePos.toString (sright s)^"\n")
|
||||
else app note_adjusteds (sub_stmts s)
|
||||
fun note_bi (BI_Stmt s) = note_adjusteds s
|
||||
| note_bi _ = ()
|
||||
fun note_defn (FnDefn (_,_,_,body))
|
||||
= app note_bi (node body)
|
||||
| note_defn _ = ()
|
||||
in app note_defn ast end
|
||||
|
||||
fun unhandled_asm cse ast = let
|
||||
open Absyn
|
||||
fun warn_asm asm = K () (ProgramAnalysis.split_asm_stmt asm)
|
||||
|
@ -471,6 +489,7 @@ in
|
|||
cse_analysis "uncalledfns" print_uncalledfns,
|
||||
cse_analysis "unmodifiedglobs" print_unmodified_globals,
|
||||
ast_analysis "ast" print_ast,
|
||||
ast_analysis "adjusted_complex_fncalls" adjusted_complex_fncalls,
|
||||
ast_analysis "unhandled_asm" unhandled_asm
|
||||
]
|
||||
end
|
||||
|
|
|
@ -0,0 +1,33 @@
|
|||
/*
|
||||
* Copyright 2018, Data61, CSIRO
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(DATA61_BSD)
|
||||
*/
|
||||
|
||||
int f (void);
|
||||
|
||||
|
||||
struct two_int {
|
||||
int first; int second;
|
||||
};
|
||||
|
||||
void
|
||||
g (void) {
|
||||
|
||||
int x;
|
||||
unsigned int y;
|
||||
struct two_int t;
|
||||
int z[2];
|
||||
|
||||
x = f ();
|
||||
|
||||
y = f ();
|
||||
|
||||
t.first = f ();
|
||||
|
||||
z[0] = f ();
|
||||
}
|
|
@ -0,0 +1,28 @@
|
|||
(*
|
||||
* Copyright 2018, Data61, CSIRO
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(DATA61_BSD)
|
||||
*)
|
||||
|
||||
theory jiraver881
|
||||
|
||||
imports "../CTranslation"
|
||||
|
||||
begin
|
||||
|
||||
install_C_file "jiraver881.c"
|
||||
|
||||
context jiraver881 begin
|
||||
|
||||
(* note that x is assigned directly from f(),
|
||||
but that compound lvars and y (different notional type) are
|
||||
assigned via explicit statements. *)
|
||||
thm g_body_def
|
||||
|
||||
end
|
||||
|
||||
end
|
Loading…
Reference in New Issue