Skip to content

Commit b716558

Browse files
sipmasipma
committed
CHB:ARM: add more type constraints
1 parent 947e436 commit b716558

File tree

3 files changed

+141
-94
lines changed

3 files changed

+141
-94
lines changed

‎CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -605,7 +605,7 @@ object (self)
605605
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
606606
^ "Parameter type not recognized in call instruction"] in
607607
let xx = rewrite_expr ?restrict:(Some 4) x in
608-
(*
608+
let ptype = get_parameter_type p in
609609
let xx =
610610
if is_pointer ptype then
611611
let _ = floc#memrecorder#record_argument xx index in
@@ -618,10 +618,9 @@ object (self)
618618
TR.tfold_default
619619
(fun v -> XOp ((Xf "addressofvar"), [(XVar v)]))
620620
xx
621-
(floc#get_var_at_address ~btype:ptype xx)
621+
(floc#get_var_at_address ~btype:(ptr_deref ptype) xx)
622622
else
623623
xx in
624-
*)
625624
let rdef = get_rdef_r xvar_r in
626625
(xx :: xprs, xvar_r :: xvars, rdef :: rdefs, index + 1))
627626
([], [], [], 1) callargs in
@@ -2530,7 +2529,7 @@ object (self)
25302529
let xxdst_r =
25312530
TR.tmap
25322531
(fun v -> XOp ((Xf "addressofvar"), [(XVar v)]))
2533-
(TR.tbind (fun x -> floc#get_var_at_address x) xxdst_r) in
2532+
(TR.tbind floc#get_var_at_address xxdst_r) in
25342533
let rdefs = [(get_rdef_r xsrc_r); (get_rdef_r xdst_r)] in
25352534
let _ =
25362535
TR.tfold_default
@@ -2636,6 +2635,7 @@ object (self)
26362635
let xrm_r = rm#to_expr floc in
26372636
let xxrt_r = TR.tmap rewrite_expr xrt_r in
26382637
let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
2638+
let lhsvar_r = TR.tbind floc#get_var_at_address xxaddr_r in
26392639
let rdefs =
26402640
[get_rdef_r xrn_r;
26412641
get_rdef_r xrm_r;
@@ -2644,7 +2644,7 @@ object (self)
26442644
let uses = [get_def_use_r vmem_r] in
26452645
let useshigh = [get_def_use_high_r vmem_r] in
26462646
let xprs_r = [xrn_r; xrm_r; xrt_r; xxrt_r; xaddr_r] in
2647-
let vars_r = [vmem_r] in
2647+
let vars_r = [vmem_r; lhsvar_r] in
26482648
let _ =
26492649
floc#memrecorder#record_store_r
26502650
~addr_r:xxaddr_r
@@ -2679,6 +2679,8 @@ object (self)
26792679
let xrm_r = rm#to_expr floc in
26802680
let xxrt_r = TR.tmap rewrite_expr xrt_r in
26812681
let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
2682+
let lhsvar_r =
2683+
TR.tbind (floc#get_var_at_address ~size:(Some 1)) xxaddr_r in
26822684
let rdefs =
26832685
[get_rdef_r xrn_r;
26842686
get_rdef_r xrm_r;
@@ -2695,7 +2697,7 @@ object (self)
26952697
~xpr_r:xxrt_r in
26962698
let (tagstring, args) =
26972699
mk_instrx_data_r
2698-
~vars_r:[vmem_r]
2700+
~vars_r:[vmem_r; lhsvar_r]
26992701
~xprs_r:[xrn_r; xrm_r; xrt_r; xxrt_r; xaddr_r]
27002702
~rdefs
27012703
~uses

‎CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml‎

Lines changed: 132 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -424,12 +424,12 @@ object (self)
424424
(* add constraints for argument values *)
425425
List.iter (fun (p, x) ->
426426
let ptype = get_parameter_type p in
427-
if is_register_parameter p then
428-
let regarg = TR.tget_ok (get_register_parameter_register p) in
429-
let pvar = floc#f#env#mk_register_variable regarg in
430-
let rdefs = get_variable_rdefs pvar in
431-
begin
432-
(if not (is_unknown_type ptype) then
427+
begin
428+
(if is_register_parameter p then
429+
let regarg = TR.tget_ok (get_register_parameter_register p) in
430+
let pvar = floc#f#env#mk_register_variable regarg in
431+
let rdefs = get_variable_rdefs pvar in
432+
if not (is_unknown_type ptype) then
433433
List.iter (fun rdsym ->
434434
let typevar =
435435
mk_reglhs_typevar regarg faddr rdsym#getBaseName in
@@ -444,53 +444,57 @@ object (self)
444444
begin
445445
log_no_type_constraint "BL-reg-arg" ptype;
446446
()
447-
end) rdefs);
448-
449-
(match getopt_stackaddress x with
450-
| None -> ()
451-
| Some offset ->
452-
let lhstypevar =
453-
mk_localstack_lhs_typevar offset faddr iaddr in
454-
if is_pointer ptype then
455-
let eltype = ptr_deref ptype in
456-
let atype = t_array eltype 1 in
457-
let opttc = mk_btype_constraint lhstypevar atype in
458-
match opttc with
459-
| Some tc ->
460-
begin
461-
log_type_constraint "BL-reg-arg" tc;
462-
store#add_constraint tc
463-
end
464-
| _ -> ())
465-
end
466-
467-
else if is_stack_parameter p then
468-
(log_tfold_default
469-
(log_error
470-
("Unable to retrieve stack offset from "
471-
^ (fts_parameter_to_string p)))
472-
(fun p_offset ->
473-
(log_tfold_default
474-
(log_error "Unable to get current stack pointer offset")
475-
(fun sp_offset ->
476-
let arg_offset =
477-
(sp_offset#add (mkNumerical p_offset))#neg in
478-
let typevar =
479-
mk_localstack_lhs_typevar
480-
arg_offset#toInt faddr iaddr in
481-
let opttc = mk_btype_constraint typevar ptype in
482-
match opttc with
483-
| Some tc ->
484-
begin
485-
log_type_constraint "BL-reg-arg" tc;
486-
store#add_constraint tc
487-
end
488-
| _ -> ())
489-
()
490-
(floc#get_singleton_stackpointer_offset)))
491-
()
492-
(get_stack_parameter_offset p))
493-
447+
end) rdefs
448+
else
449+
()
450+
451+
else if is_stack_parameter p then
452+
(log_tfold_default
453+
(log_error
454+
("Unable to retrieve stack offset from "
455+
^ (fts_parameter_to_string p)))
456+
(fun p_offset ->
457+
(log_tfold_default
458+
(log_error "Unable to get current stack pointer offset")
459+
(fun sp_offset ->
460+
let arg_offset =
461+
(sp_offset#add (mkNumerical p_offset))#neg in
462+
let typevar =
463+
mk_localstack_lhs_typevar
464+
arg_offset#toInt faddr iaddr in
465+
let opttc = mk_btype_constraint typevar ptype in
466+
match opttc with
467+
| Some tc ->
468+
begin
469+
log_type_constraint "BL-stack-arg" tc;
470+
store#add_constraint tc
471+
end
472+
| _ -> ())
473+
()
474+
(floc#get_singleton_stackpointer_offset)))
475+
()
476+
(get_stack_parameter_offset p))
477+
478+
else
479+
());
480+
481+
(match getopt_stackaddress x with
482+
| None -> ()
483+
| Some offset ->
484+
let lhstypevar =
485+
mk_localstack_lhs_typevar offset faddr iaddr in
486+
if is_pointer ptype then
487+
let eltype = ptr_deref ptype in
488+
let atype = t_array eltype 1 in
489+
let opttc = mk_btype_constraint lhstypevar atype in
490+
match opttc with
491+
| Some tc ->
492+
begin
493+
log_type_constraint "BL-reg-arg" tc;
494+
store#add_constraint tc
495+
end
496+
| _ -> ())
497+
end
494498
) callargs
495499

496500
end
@@ -574,6 +578,7 @@ object (self)
574578
let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in
575579
begin
576580

581+
(* variable introduction for lhs with type *)
577582
(match get_regvar_type_annotation () with
578583
| Some t ->
579584
let opttc = mk_btype_constraint rttypevar t in
@@ -586,6 +591,24 @@ object (self)
586591
| _ -> ())
587592
| _ -> ());
588593

594+
(* loaded type may be known *)
595+
(let xmem_r = memop#to_expr floc in
596+
let xrmem_r =
597+
TR.tmap (fun x -> simplify_xpr (floc#inv#rewrite_expr x)) xmem_r in
598+
let xtype_r = TR.tmap floc#get_xpr_type xrmem_r in
599+
let xtype_opt = TR.tvalue xtype_r ~default:None in
600+
match xtype_opt with
601+
| Some t ->
602+
let opttc = mk_btype_constraint rttypevar t in
603+
(match opttc with
604+
| Some tc ->
605+
begin
606+
log_type_constraint "LDR-var" tc;
607+
store#add_constraint tc
608+
end
609+
| _ -> ())
610+
| _ -> ());
611+
589612
(* LDR rt, [rn, rm] : X_rndef.load <: X_rt *)
590613
(let xrdef = get_variable_rdefs_r (rn#to_variable floc) in
591614
let rnreg = rn#to_register in
@@ -985,43 +1008,64 @@ object (self)
9851008
end
9861009

9871010
(* Store x in y --- *y := x --- X <: Y.store *)
988-
| StoreRegister (_, rt, _rn, rm, memvarop, _) when rm#is_immediate ->
1011+
| StoreRegister (_, rt, rn, rm, memvarop, _) when rm#is_immediate ->
1012+
let rnrdefs = get_variable_rdefs_r (rn#to_variable floc) in
1013+
let rnreg = rn#to_register in
1014+
let offset = rm#to_numerical#toInt in
1015+
let rtrdefs = get_variable_rdefs_r (rt#to_variable floc) in
1016+
let rtreg = rt#to_register in
9891017
let xaddr_r = memvarop#to_address floc in
9901018
let xrt_r = rt#to_expr floc in
991-
(match getopt_stackaddress_r xaddr_r with
992-
| None -> ()
993-
| Some offset ->
994-
let lhstypevar = mk_localstack_lhs_typevar offset faddr iaddr in
995-
begin
996-
(* propagate function argument type *)
997-
(match getopt_initial_argument_value_r xrt_r with
998-
| Some (rtreg, off) when off = 0 ->
999-
let rhstypevar = mk_function_typevar faddr in
1000-
let rhstypevar = add_freg_param_capability rtreg rhstypevar in
1001-
let rhstypeterm = mk_vty_term rhstypevar in
1002-
let lhstypeterm = mk_vty_term lhstypevar in
1003-
begin
1004-
log_subtype_constraint "STR-funarg" rhstypeterm lhstypeterm;
1005-
store#add_subtype_constraint rhstypeterm lhstypeterm
1006-
end
1007-
| _ -> ());
1008-
1009-
(* propagate src register type from rdefs *)
1010-
(let rtreg = rt#to_register in
1011-
let rtvar_r = rt#to_variable floc in
1012-
let rtrdefs = get_variable_rdefs_r rtvar_r in
1013-
List.iter (fun rtrdef ->
1014-
let rtaddr = rtrdef#getBaseName in
1015-
if rtaddr != "init" then
1016-
let rttypevar = mk_reglhs_typevar rtreg faddr rtaddr in
1017-
let rttypeterm = mk_vty_term rttypevar in
1018-
let lhstypeterm = mk_vty_term lhstypevar in
1019-
begin
1020-
log_subtype_constraint "STR-imm-off" rttypeterm lhstypeterm;
1021-
store#add_subtype_constraint rttypeterm lhstypeterm
1022-
end) rtrdefs)
1023-
end
1024-
)
1019+
begin
1020+
1021+
(match getopt_stackaddress_r xaddr_r with
1022+
| None -> ()
1023+
| Some offset ->
1024+
let lhstypevar = mk_localstack_lhs_typevar offset faddr iaddr in
1025+
begin
1026+
(* propagate function argument type *)
1027+
(match getopt_initial_argument_value_r xrt_r with
1028+
| Some (rtreg, off) when off = 0 ->
1029+
let rhstypevar = mk_function_typevar faddr in
1030+
let rhstypevar = add_freg_param_capability rtreg rhstypevar in
1031+
let rhstypeterm = mk_vty_term rhstypevar in
1032+
let lhstypeterm = mk_vty_term lhstypevar in
1033+
begin
1034+
log_subtype_constraint "STR-funarg" rhstypeterm lhstypeterm;
1035+
store#add_subtype_constraint rhstypeterm lhstypeterm
1036+
end
1037+
| _ -> ());
1038+
1039+
(* propagate src register type from rdefs *)
1040+
(let rtreg = rt#to_register in
1041+
let rtvar_r = rt#to_variable floc in
1042+
let rtrdefs = get_variable_rdefs_r rtvar_r in
1043+
List.iter (fun rtrdef ->
1044+
let rtaddr = rtrdef#getBaseName in
1045+
if rtaddr != "init" then
1046+
let rttypevar = mk_reglhs_typevar rtreg faddr rtaddr in
1047+
let rttypeterm = mk_vty_term rttypevar in
1048+
let lhstypeterm = mk_vty_term lhstypevar in
1049+
begin
1050+
log_subtype_constraint "STR-imm-off" rttypeterm lhstypeterm;
1051+
store#add_subtype_constraint rttypeterm lhstypeterm
1052+
end) rtrdefs)
1053+
end);
1054+
1055+
(List.iter (fun rndsym ->
1056+
let straddr = rndsym#getBaseName in
1057+
let rntypevar = mk_reglhs_typevar rnreg faddr straddr in
1058+
let rntypevar = add_load_capability ~size:4 ~offset rntypevar in
1059+
List.iter (fun rtdsym ->
1060+
let rtdloc = rtdsym#getBaseName in
1061+
let rttypevar = mk_reglhs_typevar rtreg faddr rtdloc in
1062+
let rttypeterm = mk_vty_term rttypevar in
1063+
let rntypeterm = mk_vty_term rntypevar in
1064+
begin
1065+
log_subtype_constraint "STR-imm-off" rttypeterm rntypeterm;
1066+
store#add_subtype_constraint rttypeterm rntypeterm
1067+
end) rtrdefs) rnrdefs)
1068+
end
10251069

10261070
| StoreRegisterByte (_, rt, rn, rm, _memvarop, _) when rm#is_immediate ->
10271071
let rnrdefs = get_variable_rdefs_r (rn#to_variable floc) in

‎CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1648,6 +1648,7 @@ let translate_arm_instruction
16481648
| LoadRegister (c, rt, rn, rm, mem, _) ->
16491649
let lhs_r = TR.tmap fst (rt#to_lhs floc) in
16501650
let rhs_r = mem#to_expr floc in
1651+
let rhs_r = TR.tmap floc#inv#rewrite_expr rhs_r in
16511652
let vrd = floc#env#mk_register_variable rt#to_register in
16521653
let updatecmds =
16531654
if mem#is_offset_address_writeback then

0 commit comments

Comments
 (0)