diff options
Diffstat (limited to 'backend/LTL.v')
| -rw-r--r-- | backend/LTL.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/backend/LTL.v b/backend/LTL.v index 8567a891..6dd1abd6 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -106,6 +106,17 @@ Definition return_regs (caller callee: locset) : locset := | S sl ofs ty => caller (S sl ofs ty) end. +(** [undef_caller_save_regs ls] models the effect of calling + an external function: caller-save registers can change unpredictably, + hence we set them to [Vundef]. *) + +Definition undef_caller_save_regs (ls: locset) : locset := + fun (l: loc) => + match l with + | R r => if is_callee_save r then ls (R r) else Vundef + | S sl ofs ty => ls (S sl ofs ty) + end. + (** LTL execution states. *) Inductive stackframe : Type := @@ -259,7 +270,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s ef t args res rs m rs' m', args = map (fun p => Locmap.getpair p rs) (loc_arguments (ef_sig ef)) -> external_call ef ge args m t res m' -> - rs' = Locmap.setpair (loc_result (ef_sig ef)) res rs -> + rs' = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) -> step (Callstate s (External ef) rs m) t (Returnstate s rs' m') | exec_return: forall f sp rs1 bb s rs m, |