diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-27 08:55:05 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-27 08:55:05 +0100 |
commit | 4622f49fd089ae47d0c853343cb0a05f986c962a (patch) | |
tree | bd045e1ef59d57f8e4b5f5734470cae56a4e68b7 /backend/Constprop.v | |
parent | 8d75ab2d38fa20dc7d8e3839967015cc276cd642 (diff) | |
download | compcert-4622f49fd089ae47d0c853343cb0a05f986c962a.tar.gz compcert-4622f49fd089ae47d0c853343cb0a05f986c962a.zip |
Extend annotations so that they can keep track of global variables and local variables whose address is taken.
- CminorSel, RTL: add "annot" instructions.
- CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions.
- AST, Events: simplify EF_annot because constants are now part of the arguments.
Implementation is not complete yet.
Diffstat (limited to 'backend/Constprop.v')
-rw-r--r-- | backend/Constprop.v | 36 |
1 files changed, 17 insertions, 19 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index bdfc4b17..ce56ff62 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -102,23 +102,22 @@ Definition num_iter := 10%nat. Definition successor (f: function) (ae: AE.t) (pc: node) : node := successor_rec num_iter f ae pc. -Fixpoint annot_strength_reduction - (ae: AE.t) (targs: list annot_arg) (args: list reg) := - match targs, args with - | AA_arg ty :: targs', arg :: args' => - let (targs'', args'') := annot_strength_reduction ae targs' args' in - match ty, areg ae arg with - | Tint, I n => (AA_int n :: targs'', args'') - | Tfloat, F n => if Compopts.generate_float_constants tt - then (AA_float n :: targs'', args'') - else (AA_arg ty :: targs'', arg :: args'') - | _, _ => (AA_arg ty :: targs'', arg :: args'') +Fixpoint annot_strength_reduction (ae: AE.t) (a: annot_arg reg) := + match a with + | AA_base r => + match areg ae r with + | I n => AA_int n + | L n => AA_long n + | F n => if Compopts.generate_float_constants tt then AA_float n else a + | FS n => if Compopts.generate_float_constants tt then AA_single n else a + | _ => a end - | targ :: targs', _ => - let (targs'', args'') := annot_strength_reduction ae targs' args in - (targ :: targs'', args'') - | _, _ => - (targs, args) + | AA_longofwords hi lo => + match annot_strength_reduction ae hi, annot_strength_reduction ae lo with + | AA_int nhi, AA_int nlo => AA_long (Int64.ofwords nhi nlo) + | hi', lo' => AA_longofwords hi' lo' + end + | _ => a end. Function builtin_strength_reduction @@ -134,9 +133,6 @@ Function builtin_strength_reduction | Ptr(Gl symb n1) => (EF_vstore_global chunk symb n1, r2 :: nil) | _ => (ef, args) end - | EF_annot text targs, args => - let (targs', args') := annot_strength_reduction ae targs args in - (EF_annot text targs', args') | _, _ => (ef, args) end. @@ -180,6 +176,8 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) | Ibuiltin ef args res s => let (ef', args') := builtin_strength_reduction ae ef args in Ibuiltin ef' args' res s + | Iannot ef args s => + Iannot ef (List.map (annot_strength_reduction ae) args) s | Icond cond args s1 s2 => let aargs := aregs ae args in match resolve_branch (eval_static_condition cond aargs) with |