diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-04-01 18:28:02 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-04-01 18:28:02 +0200 |
commit | 95ba79b10e832025bbc9843f9d14614f7dff0fcb (patch) | |
tree | 8ca03b99cf6be2aab8c7b266196569019a2a7f13 /backend/Deadcode.v | |
parent | 68e2ce02f8d69b26c9cea6e0d338f855cbea3ace (diff) | |
parent | e11b3b885a6d359925b86743b89698cc6757157a (diff) | |
download | compcert-95ba79b10e832025bbc9843f9d14614f7dff0fcb.tar.gz compcert-95ba79b10e832025bbc9843f9d14614f7dff0fcb.zip |
Merge pull request #34 from AbsInt/extended-annotations
Extended annotations
Diffstat (limited to 'backend/Deadcode.v')
-rw-r--r-- | backend/Deadcode.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/backend/Deadcode.v b/backend/Deadcode.v index 98bc14a8..9a8f85d2 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -70,6 +70,17 @@ Definition is_dead (v: nval) := Definition is_int_zero (v: nval) := match v with I n => Int.eq n Int.zero | _ => false end. +Fixpoint transfer_annot_arg (na: NA.t) (a: annot_arg reg) : NA.t := + let (ne, nm) := na in + match a with + | AA_base r => (add_need_all r ne, nm) + | AA_int _ | AA_long _ | AA_float _ | AA_single _ + | AA_addrstack _ | AA_addrglobal _ _ => (ne, nm) + | AA_loadstack chunk ofs => (ne, nmem_add nm (Stk ofs) (size_chunk chunk)) + | AA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk)) + | AA_longofwords hi lo => transfer_annot_arg (transfer_annot_arg na hi) lo + end. + Function transfer_builtin (app: VA.t) (ef: external_function) (args: list reg) (res: reg) (ne: NE.t) (nm: nmem) : NA.t := match ef, args with @@ -128,6 +139,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t) nmem_dead_stack f.(fn_stacksize)) | Some(Ibuiltin ef args res s) => transfer_builtin approx!!pc ef args res ne nm + | Some(Iannot ef args s) => + List.fold_left transfer_annot_arg args after | Some(Icond cond args s1 s2) => (add_needs args (needs_of_condition cond) ne, nm) | Some(Ijumptable arg tbl) => |