diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-06-15 15:11:26 +0200 |
---|---|---|
committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-07-06 15:41:51 +0200 |
commit | dff22ef6d855973e0e0f05c7203a6bfa9a4cf01a (patch) | |
tree | 82c09b8cff023557084d6257acdef84b1311dd35 /common/AST.v | |
parent | 92fc8a425034abc1247203a4c0d471e8b6d0e941 (diff) | |
download | compcert-dff22ef6d855973e0e0f05c7203a6bfa9a4cf01a.tar.gz compcert-dff22ef6d855973e0e0f05c7203a6bfa9a4cf01a.zip |
Extend builtin arguments with a pointer addition operator
This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses.
Current status: x86 port only, the only new addressing mode handled is reg + offset.
Diffstat (limited to 'common/AST.v')
-rw-r--r-- | common/AST.v | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/common/AST.v b/common/AST.v index 8a46a153..9eeca5b1 100644 --- a/common/AST.v +++ b/common/AST.v @@ -627,7 +627,8 @@ Inductive builtin_arg (A: Type) : Type := | BA_addrstack (ofs: ptrofs) | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: ptrofs) | BA_addrglobal (id: ident) (ofs: ptrofs) - | BA_splitlong (hi lo: builtin_arg A). + | BA_splitlong (hi lo: builtin_arg A) + | BA_addptr (a1 a2: builtin_arg A). Inductive builtin_res (A: Type) : Type := | BR (x: A) @@ -639,6 +640,7 @@ Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident := | BA_loadglobal chunk id ofs => id :: nil | BA_addrglobal id ofs => id :: nil | BA_splitlong hi lo => globals_of_builtin_arg hi ++ globals_of_builtin_arg lo + | BA_addptr a1 a2 => globals_of_builtin_arg a1 ++ globals_of_builtin_arg a2 | _ => nil end. @@ -649,6 +651,7 @@ Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A := match a with | BA x => x :: nil | BA_splitlong hi lo => params_of_builtin_arg hi ++ params_of_builtin_arg lo + | BA_addptr a1 a2 => params_of_builtin_arg a1 ++ params_of_builtin_arg a2 | _ => nil end. @@ -675,6 +678,8 @@ Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_ar | BA_addrglobal id ofs => BA_addrglobal id ofs | BA_splitlong hi lo => BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo) + | BA_addptr a1 a2 => + BA_addptr (map_builtin_arg f a1) (map_builtin_arg f a2) end. Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B := @@ -691,17 +696,5 @@ Inductive builtin_arg_constraint : Type := | OK_default | OK_const | OK_addrstack - | OK_addrglobal - | OK_addrany + | OK_addressing | OK_all. - -Definition builtin_arg_ok - (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := - match ba, c with - | (BA _ | BA_splitlong (BA _) (BA _)), _ => true - | (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const => true - | BA_addrstack _, (OK_addrstack | OK_addrany) => true - | BA_addrglobal _ _, (OK_addrglobal | OK_addrany) => true - | _, OK_all => true - | _, _ => false - end. |