From dff22ef6d855973e0e0f05c7203a6bfa9a4cf01a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 15 Jun 2017 15:11:26 +0200 Subject: 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. --- backend/Stacking.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backend/Stacking.v') diff --git a/backend/Stacking.v b/backend/Stacking.v index f51848f2..7b382d05 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -97,6 +97,8 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m | BA_addrglobal id ofs => BA_addrglobal id ofs | BA_splitlong hi lo => BA_splitlong (transl_builtin_arg fe hi) (transl_builtin_arg fe lo) + | BA_addptr a1 a2 => + BA_addptr (transl_builtin_arg fe a1) (transl_builtin_arg fe a2) end. (** Translation of a Linear instruction. Prepends the corresponding -- cgit