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 /x86/Op.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 'x86/Op.v')
-rw-r--r-- | x86/Op.v | 21 |
1 files changed, 21 insertions, 0 deletions
@@ -1455,3 +1455,24 @@ Proof. Qed. End EVAL_INJECT. + +(** * Handling of builtin arguments *) + +Definition builtin_arg_ok_1 + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match c, ba with + | OK_all, _ => true + | OK_const, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => true + | OK_addrstack, BA_addrstack _ => true + | OK_addressing, BA_addrstack _ => true + | OK_addressing, BA_addrglobal _ _ => true + | OK_addressing, BA_addptr (BA _) (BA_int _ | BA_long _) => true + | _, _ => false + end. + +Definition builtin_arg_ok + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match ba with + | (BA _ | BA_splitlong (BA _) (BA _)) => true + | _ => builtin_arg_ok_1 ba c + end. |