diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-06 19:38:53 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-06 19:38:53 +0200 |
commit | dba05a9f6259c82a350987b511bf1a71f113d0ba (patch) | |
tree | 6e7fee8d65b6a180447267da9a95a93827443caf /ia32/Machregs.v | |
parent | 108db39b8b7c1d42cbc38c5aabf885ef5440f189 (diff) | |
parent | 47d0e5256ab79b402faae14260fa2fabc1d24dcb (diff) | |
download | compcert-dba05a9f6259c82a350987b511bf1a71f113d0ba.tar.gz compcert-dba05a9f6259c82a350987b511bf1a71f113d0ba.zip |
X
Merge branch 'master' into debug_locations
Diffstat (limited to 'ia32/Machregs.v')
-rw-r--r-- | ia32/Machregs.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v index 65e27599..ace193b7 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -137,7 +137,6 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := | EF_memcpy sz al => if zle sz 32 then CX :: X7 :: nil else CX :: SI :: DI :: nil | EF_vstore (Mint8unsigned|Mint8signed) => AX :: CX :: nil - | EF_vstore_global (Mint8unsigned|Mint8signed) _ _ => AX :: nil | EF_builtin id sg => if ident_eq id builtin_write16_reversed || ident_eq id builtin_write32_reversed @@ -267,3 +266,15 @@ Definition two_address_op (op: operation) : bool := | Ocmp c => false end. +(* Constraints on constant propagation for builtins *) + +Definition builtin_constraints (ef: external_function) : + list builtin_arg_constraint := + match ef with + | EF_vload _ => OK_addrany :: nil + | EF_vstore _ => OK_addrany :: OK_default :: nil + | EF_memcpy _ _ => OK_addrany :: OK_addrany :: nil + | EF_annot txt targs => map (fun _ => OK_all) targs + | EF_debug kind txt targs => map (fun _ => OK_all) targs + | _ => nil + end. |