Skip to content

Commit fe5c470

Browse files
sipmasipma
committed
CHB:ARM:TYPE: exclude stackpointer from typing rules
1 parent d6dcdfb commit fe5c470

File tree

2 files changed

+65
-54
lines changed

2 files changed

+65
-54
lines changed

‎CodeHawk/CHB/bchlib/bCHVersion.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -95,8 +95,8 @@ end
9595

9696

9797
let version = new version_info_t
98-
~version:"0.6.0_20250728"
99-
~date:"2025-07-28"
98+
~version:"0.6.0_20250729"
99+
~date:"2025-07-29"
100100
~licensee: None
101101
~maxfilesize: None
102102
()

‎CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml‎

Lines changed: 63 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -389,21 +389,25 @@ object (self)
389389
let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in
390390
let rndefs = get_variable_rdefs_r (rn#to_variable floc) in
391391
let rnreg = rn#to_register in
392-
List.iter (fun rnsym ->
393-
let rnaddr = rnsym#getBaseName in
394-
let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in
395-
let rntypeterm = mk_vty_term rntypevar in
396-
let lhstypeterm = mk_vty_term lhstypevar in
397-
let rule = "ADD-c" in
398-
if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then
399-
begin
400-
log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm;
401-
store#add_subtype_constraint
402-
faddr iaddr rule rntypeterm lhstypeterm
403-
end
404-
else
405-
log_subtype_rule_disabled __LINE__ rule rntypeterm lhstypeterm
406-
) rndefs);
392+
if rn#is_sp_register || rd#is_sp_register then
393+
(* no information to be gained from stack pointer manipulations *)
394+
()
395+
else
396+
List.iter (fun rnsym ->
397+
let rnaddr = rnsym#getBaseName in
398+
let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in
399+
let rntypeterm = mk_vty_term rntypevar in
400+
let lhstypeterm = mk_vty_term lhstypevar in
401+
let rule = "ADD-c" in
402+
if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then
403+
begin
404+
log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm;
405+
store#add_subtype_constraint
406+
faddr iaddr rule rntypeterm lhstypeterm
407+
end
408+
else
409+
log_subtype_rule_disabled __LINE__ rule rntypeterm lhstypeterm
410+
) rndefs);
407411

408412
(match getopt_global_address_r (rn#to_expr floc) with
409413
| Some gaddr ->
@@ -979,24 +983,28 @@ object (self)
979983
(regvar_linked_to_exit "LDRB" rt);
980984

981985
(* LDRB rt, [rn, rm] : X_rndef.load <: X_rt *)
982-
(let xrdefs = get_variable_rdefs_r (rn#to_variable floc) in
983-
let rnreg = rn#to_register in
984-
let offset = rm#to_numerical#toInt in
985-
List.iter (fun rdsym ->
986-
let ldaddr = rdsym#getBaseName in
987-
let rdtypevar = mk_reglhs_typevar rnreg faddr ldaddr in
988-
let rdtypevar = add_load_capability ~offset ~size:1 rdtypevar in
989-
let rdtypeterm = mk_vty_term rdtypevar in
990-
let rttypeterm = mk_vty_term rttypevar in
991-
let rule = "LDRB-load" in
992-
if fndata#is_typing_rule_enabled ~rdef:(Some ldaddr) iaddr rule then
993-
begin
994-
log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm;
995-
store#add_subtype_constraint faddr iaddr rule rdtypeterm rttypeterm
996-
end
997-
else
998-
log_subtype_rule_disabled __LINE__ rule rdtypeterm rttypeterm
999-
) xrdefs);
986+
(if rn#is_sp_register then
987+
()
988+
else
989+
let xrdefs = get_variable_rdefs_r (rn#to_variable floc) in
990+
let rnreg = rn#to_register in
991+
let offset = rm#to_numerical#toInt in
992+
List.iter (fun rdsym ->
993+
let ldaddr = rdsym#getBaseName in
994+
let rdtypevar = mk_reglhs_typevar rnreg faddr ldaddr in
995+
let rdtypevar = add_load_capability ~offset ~size:1 rdtypevar in
996+
let rdtypeterm = mk_vty_term rdtypevar in
997+
let rttypeterm = mk_vty_term rttypevar in
998+
let rule = "LDRB-load" in
999+
if fndata#is_typing_rule_enabled ~rdef:(Some ldaddr) iaddr rule then
1000+
begin
1001+
log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm;
1002+
store#add_subtype_constraint
1003+
faddr iaddr rule rdtypeterm rttypeterm
1004+
end
1005+
else
1006+
log_subtype_rule_disabled __LINE__ rule rdtypeterm rttypeterm
1007+
) xrdefs);
10001008

10011009
(* LDRB rt, ... : X_rt <: integer type *)
10021010
(let tc = mk_int_type_constant Unsigned 8 in
@@ -1455,25 +1463,28 @@ object (self)
14551463
end);
14561464

14571465
(let rule = "STR-store" in
1458-
List.iter (fun rndsym ->
1459-
let straddr = rndsym#getBaseName in
1460-
let rntypevar = mk_reglhs_typevar rnreg faddr straddr in
1461-
let rntypevar = add_store_capability ~size:4 ~offset rntypevar in
1462-
List.iter (fun rtdsym ->
1463-
let rtdloc = rtdsym#getBaseName in
1464-
let rttypevar = mk_reglhs_typevar rtreg faddr rtdloc in
1465-
let rttypeterm = mk_vty_term rttypevar in
1466-
let rntypeterm = mk_vty_term rntypevar in
1467-
if fndata#is_typing_rule_enabled
1468-
~rdef:(Some rtdloc) iaddr rule then
1469-
begin
1470-
log_subtype_constraint __LINE__ rule rttypeterm rntypeterm;
1471-
store#add_subtype_constraint
1472-
faddr iaddr rule rttypeterm rntypeterm
1473-
end
1474-
else
1475-
log_subtype_rule_disabled __LINE__ rule rttypeterm rntypeterm
1476-
) rtrdefs) rnrdefs);
1466+
if rn#is_sp_register then
1467+
()
1468+
else
1469+
List.iter (fun rndsym ->
1470+
let straddr = rndsym#getBaseName in
1471+
let rntypevar = mk_reglhs_typevar rnreg faddr straddr in
1472+
let rntypevar = add_store_capability ~size:4 ~offset rntypevar in
1473+
List.iter (fun rtdsym ->
1474+
let rtdloc = rtdsym#getBaseName in
1475+
let rttypevar = mk_reglhs_typevar rtreg faddr rtdloc in
1476+
let rttypeterm = mk_vty_term rttypevar in
1477+
let rntypeterm = mk_vty_term rntypevar in
1478+
if fndata#is_typing_rule_enabled
1479+
~rdef:(Some rtdloc) iaddr rule then
1480+
begin
1481+
log_subtype_constraint __LINE__ rule rttypeterm rntypeterm;
1482+
store#add_subtype_constraint
1483+
faddr iaddr rule rttypeterm rntypeterm
1484+
end
1485+
else
1486+
log_subtype_rule_disabled __LINE__ rule rttypeterm rntypeterm
1487+
) rtrdefs) rnrdefs);
14771488

14781489
(* type of destination memory location may be known *)
14791490
(let vmem_r = memvarop#to_variable floc in

0 commit comments

Comments
 (0)