diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-01 09:57:01 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-01 09:57:01 +0200 |
commit | 951963b380f1ff1e0b55f8303e4ae098cedb3cb5 (patch) | |
tree | 6cc793efe8fc8d2950d7b313bfde79b2ecf40d24 /backend/Inliningspec.v | |
parent | 7cfaf10b604372044f53cb65b03df33c23f8b26d (diff) | |
parent | 3324ece265091490d5380caf753d76aeee059d3f (diff) | |
download | compcert-951963b380f1ff1e0b55f8303e4ae098cedb3cb5.tar.gz compcert-951963b380f1ff1e0b55f8303e4ae098cedb3cb5.zip |
Merge branch 'new-builtins'
Diffstat (limited to 'backend/Inliningspec.v')
-rw-r--r-- | backend/Inliningspec.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index f7e6c317..161e2a6e 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -313,12 +313,9 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop := context_stack_tailcall ctx f ctx' -> tr_instr ctx pc (Itailcall sg (inr _ id) args) c | tr_builtin: forall ctx pc c ef args res s, - Ple res ctx.(mreg) -> - c!(spc ctx pc) = Some (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s)) -> + match res with BR r => Ple r ctx.(mreg) | _ => True end -> + c!(spc ctx pc) = Some (Ibuiltin ef (map (sbuiltinarg ctx) args) (sbuiltinres ctx res) (spc ctx s)) -> tr_instr ctx pc (Ibuiltin ef args res s) c - | tr_annot: forall ctx pc c ef args s, - c!(spc ctx pc) = Some (Iannot ef (map (sannotarg ctx) args) (spc ctx s)) -> - tr_instr ctx pc (Iannot ef args s) c | tr_cond: forall ctx pc cond args s1 s2 c, c!(spc ctx pc) = Some (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) -> tr_instr ctx pc (Icond cond args s1 s2) c @@ -554,6 +551,8 @@ Proof. red; simpl. subst s2; simpl in *; xomega. red; auto. +(* builtin *) + eapply tr_builtin; eauto. destruct b; eauto. (* return *) destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. (* inlined *) |