Skip to content

Commit 46ab5ba

Browse files
sipmasipma
committed
CHB: redo resolution of fixed-offset indirect memory access
1 parent 8681db4 commit 46ab5ba

File tree

3 files changed

+227
-15
lines changed

3 files changed

+227
-15
lines changed

‎CodeHawk/CHB/bchlib/bCHFloc.ml‎

Lines changed: 187 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -403,16 +403,6 @@ object (self)
403403

404404
method memrecorder = mk_memory_recorder self#f self#cia
405405

406-
(* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
407-
* return values *
408-
* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
409-
(*
410-
method record_return_value =
411-
let eax = self#env#mk_cpu_register_variable Eax in
412-
let returnExpr = self#rewrite_variable_to_external eax in
413-
self#f#record_return_value self#cia returnExpr
414-
*)
415-
416406
(* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
417407
* call targets *
418408
* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
@@ -643,11 +633,67 @@ object (self)
643633
* resolve and save IndReg (cpureg, offset) (memrefs1)
644634
* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
645635

636+
method get_memory_variable_numoffset
637+
?(align=1)
638+
?(size=4)
639+
(var: variable_t)
640+
(numoffset: numerical_t): variable_t traceresult =
641+
let inv = self#inv in
642+
if inv#is_base_offset_constant var then
643+
let (base, offset) = inv#get_base_offset_constant var in
644+
let memoffset = numoffset#add offset in
645+
TR.tmap
646+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
647+
(fun memref -> self#env#mk_memory_variable ~size memref memoffset)
648+
(self#env#mk_base_sym_reference base)
649+
else
650+
let varx =
651+
if align > 1 then
652+
let alignx = int_constant_expr align in
653+
XOp (XMult, [XOp (XDiv, [XVar var; alignx]); alignx])
654+
else
655+
XVar var in
656+
let addr = XOp (XPlus, [varx; num_constant_expr numoffset]) in
657+
let address = inv#rewrite_expr addr in
658+
match address with
659+
| XConst (IntConst n) ->
660+
let dw = numerical_mod_to_doubleword n in
661+
if system_info#get_image_base#le dw then
662+
tprop
663+
(self#env#mk_global_variable ~size n)
664+
(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
665+
else
666+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
667+
^ "Unable to convert constant value " ^ n#toString
668+
^ "to a valid program address (should be greater than "
669+
^ system_info#get_image_base#to_hex_string
670+
^ ")"]
671+
| _ ->
672+
let (memref_r, memoffset_r) = self#decompose_memaddr address in
673+
tbind
674+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
675+
(fun memref ->
676+
if memref#is_global_reference then
677+
tbind
678+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
679+
(fun memoff ->
680+
self#env#mk_global_variable (get_total_constant_offset memoff))
681+
memoffset_r
682+
else
683+
tmap
684+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
685+
(fun memoff ->
686+
(self#env#mk_memory_variable
687+
memref (get_total_constant_offset memoff)))
688+
memoffset_r)
689+
memref_r
690+
691+
646692
method get_memory_variable_1
647693
?(align=1) (* alignment of var value *)
648694
?(size=4)
649695
(var:variable_t)
650-
(offset:numerical_t) =
696+
(offset:numerical_t): variable_t =
651697
let default () =
652698
self#env#mk_memory_variable
653699
(self#env#mk_unknown_memory_reference "memref-1") offset in
@@ -1120,6 +1166,136 @@ object (self)
11201166
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
11211167
^ "Unable to create global variable for " ^ (x2s addrvalue)]
11221168

1169+
method decompose_memaddr (x: xpr_t):
1170+
(memory_reference_int traceresult * memory_offset_t traceresult) =
1171+
let is_external (v: variable_t) = self#env#is_function_initial_value v in
1172+
let vars = vars_as_positive_terms x in
1173+
let knownpointers = List.filter self#f#is_base_pointer vars in
1174+
match knownpointers with
1175+
(* one known pointer, must be the base *)
1176+
| [base] ->
1177+
let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
1178+
let memref_r = self#env#mk_base_variable_reference base in
1179+
let memoff_r =
1180+
(match offset with
1181+
| XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
1182+
| XOp (XMult, [XConst (IntConst n); XVar v]) ->
1183+
Ok (IndexOffset (v, n#toInt, NoOffset))
1184+
| _ ->
1185+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1186+
^ "Offset not recognized: " ^ (x2s offset)]) in
1187+
(memref_r, memoff_r)
1188+
1189+
(* no known pointers, have to find a base *)
1190+
| [] ->
1191+
let maxC = largest_constant_term x in
1192+
if maxC#gt system_info#get_image_base#to_numerical then
1193+
(* global base *)
1194+
let memref_r = Ok self#env#mk_global_memory_reference in
1195+
let offset = simplify_xpr (XOp (XMinus, [x; num_constant_expr maxC])) in
1196+
let gmemoff_r =
1197+
match offset with
1198+
| XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
1199+
| XOp (XMult, [XConst (IntConst n); XVar v]) ->
1200+
Ok (IndexOffset (v, n#toInt, NoOffset))
1201+
| XOp (XMult, [XConst (IntConst n); x])
1202+
when self#is_composite_symbolic_value x ->
1203+
let v = self#env#mk_symbolic_value x in
1204+
Ok (IndexOffset (v, n#toInt, NoOffset))
1205+
| _ ->
1206+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1207+
^ "Offset not recognized: " ^ (x2s offset)] in
1208+
let memoff_r =
1209+
tmap
1210+
(fun gmemoff -> ConstantOffset (maxC, gmemoff))
1211+
gmemoff_r in
1212+
(memref_r, memoff_r)
1213+
1214+
else
1215+
(* find a candidate base pointer *)
1216+
(match vars with
1217+
| [base] when (self#is_initial_value_variable base)
1218+
|| (is_external base) ->
1219+
let _ = self#f#add_base_pointer base in
1220+
let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
1221+
let memref_r = self#env#mk_base_variable_reference base in
1222+
let memoff_r =
1223+
match offset with
1224+
| XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
1225+
| XOp (XMult, [XConst (IntConst n); XVar v]) ->
1226+
Ok (IndexOffset (v, n#toInt, NoOffset))
1227+
| _ ->
1228+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1229+
^ "Offset not recognized: " ^ (x2s offset)] in
1230+
(memref_r, memoff_r)
1231+
1232+
| [base] when (self#env#is_stack_parameter_variable base)
1233+
&& (self#f#env#has_constant_offset base)
1234+
&& (self#has_initial_value base) ->
1235+
let base_r =
1236+
TR.tmap
1237+
(fun baseInit ->
1238+
let _ = self#f#add_base_pointer baseInit in
1239+
baseInit)
1240+
(self#f#env#mk_initial_memory_value base) in
1241+
let memref_r =
1242+
TR.tbind
1243+
(fun base -> self#env#mk_base_variable_reference base)
1244+
base_r in
1245+
let memoff_r =
1246+
TR.tbind
1247+
(fun base ->
1248+
let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
1249+
match offset with
1250+
| XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
1251+
| XOp (XMult, [XConst (IntConst n); XVar v]) ->
1252+
Ok (IndexOffset (v, n#toInt, NoOffset))
1253+
| _ ->
1254+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1255+
^ "Offset not recognized: " ^ (x2s offset)])
1256+
base_r in
1257+
(memref_r, memoff_r)
1258+
1259+
| [v] ->
1260+
let memref_r =
1261+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1262+
^ "No candidate base pointers. Only variable found: "
1263+
^ (p2s v#toPretty)] in
1264+
let memoff_r =
1265+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__)] in
1266+
(memref_r, memoff_r)
1267+
1268+
| [] ->
1269+
let memref_r =
1270+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1271+
^ "No candidate pointers. Left with maxC: "
1272+
^ maxC#toString] in
1273+
let memoff_r =
1274+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__)] in
1275+
(memref_r, memoff_r)
1276+
1277+
(* multiple variables *)
1278+
| _ ->
1279+
let memref_r =
1280+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1281+
^ "Multiple variables: "
1282+
^ (String.concat "; "
1283+
(List.map (fun v -> p2s v#toPretty) vars))] in
1284+
let memoff_r =
1285+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__)] in
1286+
(memref_r, memoff_r))
1287+
1288+
(* multiple known pointers *)
1289+
| _ ->
1290+
let memref_r =
1291+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1292+
^ "Multiple known pointers: "
1293+
^ (String.concat "; "
1294+
(List.map (fun v -> p2s v#toPretty) knownpointers))] in
1295+
let memoff_r =
1296+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__)] in
1297+
(memref_r, memoff_r)
1298+
11231299
(* the objective is to extract a base pointer and an offset expression
11241300
* first check whether the expression contains any variables that are known
11251301
* base pointers;

‎CodeHawk/CHB/bchlib/bCHLibTypes.mli‎

Lines changed: 39 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5757,10 +5757,33 @@ class type floc_int =
57575757

57585758
(** {2 Resolve memory variable}*)
57595759

5760+
(** [get_memory_variable_numoffset var num] returns the variable that
5761+
corresponds to the address expression [var + num].
5762+
5763+
This method is convenient for indirect memory accesses expressed by
5764+
a register base and immediate offset.
5765+
5766+
This method should eventually replace [get_memory_variable_1]
5767+
*)
5768+
method get_memory_variable_numoffset:
5769+
?align:int
5770+
-> ?size:int
5771+
-> variable_t
5772+
-> numerical_t
5773+
-> variable_t traceresult
5774+
57605775
(* returns the memory reference corresponding to the address in
5761-
variable plus offset *)
5776+
variable plus offset.
5777+
5778+
Deprecated. Should eventually be replaced by
5779+
[get_memory_variable_numoffset].
5780+
*)
57625781
method get_memory_variable_1:
5763-
?align:int -> ?size:int -> variable_t -> numerical_t -> variable_t
5782+
?align:int
5783+
-> ?size:int
5784+
-> variable_t
5785+
-> numerical_t
5786+
-> variable_t
57645787

57655788
(* returns the memory reference corresponding to a base and index
57665789
variable plus offset *)
@@ -5781,7 +5804,20 @@ class type floc_int =
57815804
index variable *)
57825805
method get_memory_variable_4: variable_t -> int -> numerical_t -> variable_t
57835806

5784-
(* returns the memory reference that corresponds to the address expression *)
5807+
(* [decompose_memaddr addr] attempts to separate the terms of [addr] into
5808+
a base (global, stack, or base variable) and an offset.
5809+
5810+
This method should eventually replace the method [decompose_address].
5811+
*)
5812+
method decompose_memaddr:
5813+
xpr_t
5814+
-> (memory_reference_int traceresult * memory_offset_t traceresult)
5815+
5816+
(* returns the memory reference and offset that corresponds to the address
5817+
expression.
5818+
5819+
Deprecated. Should eventually be replaced by [decompose_memaddr]
5820+
*)
57855821
method decompose_address: xpr_t -> (memory_reference_int * memory_offset_t)
57865822

57875823
(* returns the variable associated with the address expression *)

‎CodeHawk/CHB/bchlib/bCHVariable.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -613,7 +613,7 @@ object (self)
613613
method make_memref_from_basevar
614614
(v: variable_t): memory_reference_int traceresult =
615615
tbind
616-
~msg:"make_memref_from_basevar_basevar"
616+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
617617
(fun av ->
618618
match av#to_basevar_reference with
619619
| Some memref -> Ok memref

0 commit comments

Comments
 (0)