Skip to content

Commit c888f84

Browse files
committed
CHB: add type constraints
1 parent 7266c27 commit c888f84

File tree

4 files changed

+413
-101
lines changed

4 files changed

+413
-101
lines changed

CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -666,6 +666,13 @@ object (self:'a)
666666
XOp
667667
(XLsl,
668668
[XVar (env#mk_arm_register_variable r); int_constant_expr n])
669+
| ARMShiftedReg (r, ARMRegSRT (SRType_LSL, sr)) ->
670+
let env = floc#f#env in
671+
let shiftv =
672+
XOp (XBAnd,
673+
[XVar (env#mk_arm_register_variable sr);
674+
int_constant_expr 7]) in
675+
XOp (XLsl, [XVar (env#mk_arm_register_variable r); shiftv])
669676
| ARMShiftedReg _ ->
670677
let _ =
671678
chlog#add

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1243,7 +1243,8 @@ object (self)
12431243
let vrn = rn#to_variable floc in
12441244
let addr_r = mem#to_updated_offset_address floc in
12451245
log_tfold_default
1246-
(log_error "invalid write-back address" ((p2s floc#l#toPretty) ^ ": LDR"))
1246+
(log_error
1247+
"invalid write-back address" ((p2s floc#l#toPretty) ^ ": LDR"))
12471248
(fun (inc, xaddr) -> add_base_update tags args vrn inc xaddr)
12481249
(tags, args)
12491250
addr_r
@@ -1518,7 +1519,11 @@ object (self)
15181519
("a:" :: ["subsumed"; ctxtva], [])
15191520
| _ -> (["a:"], []))
15201521

1521-
| Move(_, c, rd, rm, _, _) ->
1522+
| Move (_, _, rd, rm, _, _)
1523+
when rm#is_register && rd#get_register = rm#get_register ->
1524+
(["nop"], [])
1525+
1526+
| Move (_, c, rd, rm, _, _) ->
15221527
let vrd = rd#to_variable floc in
15231528
let xrm = rm#to_expr floc in
15241529
let result = rewrite_expr ?restrict:(Some 4) xrm in

0 commit comments

Comments
 (0)