From 626ea26cb58e50e7a42f90a6e23218d90df6dd5a Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 20 Aug 2014 14:24:42 +0000 Subject: Add builtins for load with reservation and conditional store. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Check.ml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'checklink') diff --git a/checklink/Check.ml b/checklink/Check.ml index a9a5f02..f175f16 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -1664,6 +1664,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Plwarx(rd, r1, r2) -> + begin match ecode with + | LWARX(rD, rA, rB):: es -> + OK(fw) + >>= match_iregs rd rD + >>= match_iregs r1 rA + >>= match_iregs r2 rB + >>= recur_simpl + | _ -> error + end | Plwbrx(rd, r1, r2) -> begin match ecode with | LWBRX(rD, rA, rB):: es -> @@ -2121,6 +2131,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pstwcx_(rd, r1, r2) -> + begin match ecode with + | STWCX_(rS, rA, rB) :: es -> + OK(fw) + >>= match_iregs rd rS + >>= match_iregs r1 rA + >>= match_iregs r2 rB + >>= recur_simpl + | _ -> error + end | Pstwxu(rd, r1, r2) -> begin match ecode with | STWUX(rS, rA, rB) :: es -> -- cgit v1.2.3