summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-04-12 21:57:31 +0000
committerGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-04-12 21:57:31 +0000
commitacec11c3a6f9364eaabe398de6e65ccff510bf39 (patch)
tree05cc0dac9087c2a0ac59fa29c5780b1348541fb9
parentcf3240e47400afd9485c596b65171e6dbc53ffcf (diff)
Added long versions of Pbf and Pbt
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1877 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--checklink/Check.ml122
1 files changed, 80 insertions, 42 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml
index abae47b..c2bade7 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -720,6 +720,38 @@ let match_memcpy_big ecode pc sz al src dst fw
)
| _ -> None
+let match_bo_bt_bool bo =
+ bitmatch bo with
+ | { false:1; true:1; true:1; false:1; false:1 } -> true
+ | { _ } -> false
+
+let match_bo_bf_bool bo =
+ bitmatch bo with
+ | { false:1; false:1; true:1; false:1; false:1 } -> true
+ | { _ } -> false
+
+let match_bo_bt bo ffw =
+ ffw >>> (ff_ef ^%=
+ bitmatch bo with
+ | { false:1; true:1; true:1; false:1; false:1 } -> id
+ | { _ } -> add_log (ERROR("match_bo_bt"))
+ )
+
+let match_bo_bf bo ffw =
+ ffw >>> (ff_ef ^%=
+ if match_bo_bf_bool bo
+ then id
+ else add_log (ERROR("match_bo_bf"))
+ )
+
+let match_bo_ctr bo ffw =
+ ffw
+ >>> (ff_ef ^%=
+ bitmatch bo with
+ | { true:1; false:1; true:1; false:1; false:1 } -> id
+ | { _ } -> add_log (ERROR("bitmatch"))
+ )
+
(** Compares a whole CompCert function code against an ELF code, starting at
program counter [pc].
*)
@@ -883,9 +915,9 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
| Bx(li, aa, lk) :: es ->
let lblvaddr = Int32.(add pc (mul 4l (exts li))) in
fw
- >>> match_bools false aa
- >>> match_bools false lk
>>> lblmap_unify lbl lblvaddr
+ >>? match_bools false aa
+ >>? match_bools false lk
>>= recur_simpl
| _ -> error
end
@@ -893,11 +925,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
begin match ecode with
| BCCTRx(bo, bi, lk) :: es ->
fw
- >>> (ff_ef ^%=
- bitmatch bo with
- | { true:1; false:1; true:1; false:1; false:1 } -> id
- | { _ } -> add_log (ERROR("bitmatch"))
- )
+ >>> match_bo_ctr bo
>>> match_ints 0 bi
>>> match_bools false lk
>>> recur_simpl
@@ -907,11 +935,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
begin match ecode with
| BCCTRx(bo, bi, lk) :: es ->
fw
- >>> (ff_ef ^%=
- bitmatch bo with
- | { true:1; false:1; true:1; false:1; false:1 } -> id
- | { _ } -> add_log (ERROR("bitmatch"))
- )
+ >>> match_bo_ctr bo
>>> match_ints 0 bi
>>> match_bools true lk
>>> recur_simpl
@@ -919,19 +943,30 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
end
| Pbf(bit, lbl) ->
begin match ecode with
- | BCx(bo, bi, bd, aa, lk) :: es ->
+ | BCx(bo, bi, bd, aa, lk) :: es when match_bo_bf_bool bo ->
let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in
fw
- >>> (ff_ef ^%=
- bitmatch bo with
- | { false:1; false:1; true:1; false:1; false:1 } -> id
- | { _ } -> add_log (ERROR("bitmatch"))
- )
+ (* >>> match_bo_bf bo already done in pattern match *)
>>> match_crbits bit bi
>>> lblmap_unify lbl lblvaddr
>>? match_bools false aa
>>? match_bools false lk
>>= recur_simpl
+ | BCx(bo0, bi0, bd0, aa0, lk0) ::
+ Bx (li1, aa1, lk1) :: es ->
+ let cnext = Int32.add pc 8l in
+ let enext = Int32.(add pc (mul 4l (exts bd0))) in
+ let lblvaddr = Int32.(add pc (mul 4l (exts bd0))) in
+ fw
+ >>> match_bo_bt bo0
+ >>> match_crbits bit bi0
+ >>> match_int32s cnext enext
+ >>> match_bools false aa0
+ >>> match_bools false lk0
+ >>> lblmap_unify lbl lblvaddr
+ >>? match_bools false aa1
+ >>? match_bools false lk1
+ >>= compare_code cs es (Int32.add 8l pc)
| _ -> error
end
| Pbl(ident) ->
@@ -939,9 +974,9 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
| Bx(li, aa, lk) :: es ->
let dest = Int32.(add pc (mul 4l (exts li))) in
fw
- >>> match_bools false aa
- >>> match_bools true lk
>>> (ff_sf ^%=? idmap_unify ident dest)
+ >>? match_bools false aa
+ >>? match_bools true lk
>>= recur_simpl
| _ -> error
end
@@ -949,11 +984,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
begin match ecode with
| BCLRx(bo, bi, lk) :: es ->
fw
- >>> (ff_ef ^%=
- bitmatch bo with
- | { true:1; false:1; true:1; false:1; false:1 } -> id
- | { _ } -> add_log (ERROR("bitmatch"))
- )
+ >>> match_bo_ctr bo
>>> match_ints 0 bi
>>> match_bools false lk
>>> recur_simpl
@@ -972,19 +1003,30 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
end
| Pbt(bit, lbl) ->
begin match ecode with
- | BCx(bo, bi, bd, aa, lk) :: es ->
+ | BCx(bo, bi, bd, aa, lk) :: es when match_bo_bt_bool bo ->
let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in
fw
- >>> (ff_ef ^%=
- bitmatch bo with
- | { false:1; true:1; true:1; false:1; false:1 } -> id
- | { _ } -> add_log (ERROR("bitmatch"))
- )
+ (* >>> match_bo_bt bo already done in pattern match *)
>>> match_crbits bit bi
>>> lblmap_unify lbl lblvaddr
>>? match_bools false aa
>>? match_bools false lk
>>= recur_simpl
+ | BCx(bo0, bi0, bd0, aa0, lk0) ::
+ Bx (li1, aa1, lk1) :: es ->
+ let cnext = Int32.add pc 8l in
+ let enext = Int32.(add pc (mul 4l (exts bd0))) in
+ let lblvaddr = Int32.(add pc (mul 4l (exts bd0))) in
+ fw
+ >>> match_bo_bf bo0
+ >>> match_crbits bit bi0
+ >>> match_int32s cnext enext
+ >>> match_bools false aa0
+ >>> match_bools false lk0
+ >>> lblmap_unify lbl lblvaddr
+ >>? match_bools false aa1
+ >>? match_bools false lk1
+ >>= compare_code cs es (Int32.add 8l pc)
| _ -> error
end
| Pbtbl(reg, table) ->
@@ -998,17 +1040,13 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
) in
let tblsize = (32 * List.length table) in
fw
- >>> match_iregs GPR12 rD0
- >>> match_iregs reg rA0
- >>> match_iregs GPR12 rD1
- >>> match_iregs GPR12 rA1
- >>> match_iregs GPR12 rS2
- >>> match_ctr spr2
- >>> (ff_ef ^%=
- bitmatch bo3 with
- | { true:1; false:1; true:1; false:1; false:1 } -> id
- | { _ } -> add_log (ERROR("bitmatch"))
- )
+ >>> match_iregs GPR12 rD0
+ >>> match_iregs reg rA0
+ >>> match_iregs GPR12 rD1
+ >>> match_iregs GPR12 rA1
+ >>> match_iregs GPR12 rS2
+ >>> match_ctr spr2
+ >>> match_bo_ctr bo3
>>> match_ints 0 bi3
>>> match_bools false rc3
>>> match_jmptbl table tblvaddr tblsize