Skip to content

Commit a58d1b4

Browse files
sipmasipma
committed
CHB: add more memory variable typing
1 parent ab4bd66 commit a58d1b4

File tree

5 files changed

+176
-71
lines changed

5 files changed

+176
-71
lines changed

‎CodeHawk/CHB/bchlib/bCHFloc.ml‎

Lines changed: 129 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -665,6 +665,8 @@ object (self)
665665
let xaofv_r = self#f#env#get_addressof_symbolic_expr var in
666666
let memvar_r =
667667
TR.tbind
668+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
669+
^ "var: " ^ (x2s (XVar var)))
668670
(fun xaofv ->
669671
match xaofv with
670672
| XOp ((Xf "addressofvar"), [XVar v]) -> Ok v
@@ -675,6 +677,7 @@ object (self)
675677
xaofv_r in
676678
let memoff_r =
677679
TR.tbind
680+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
678681
(fun memvar ->
679682
let memtype = self#env#get_variable_type memvar in
680683
let memtype =
@@ -684,6 +687,7 @@ object (self)
684687
address_memory_offset memtype (num_constant_expr numoffset))
685688
memvar_r in
686689
TR.tbind
690+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
687691
(fun memvar ->
688692
TR.tbind
689693
(fun memoff -> self#f#env#add_memory_offset memvar memoff)
@@ -1291,10 +1295,12 @@ object (self)
12911295
when self#f#env#is_global_variable v ->
12921296
let gvaddr_r = self#f#env#get_global_variable_address v in
12931297
TR.tbind
1298+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
12941299
(fun gvaddr ->
12951300
if memmap#has_location gvaddr then
12961301
let gloc = memmap#get_location gvaddr in
12971302
TR.tmap
1303+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
12981304
(fun offset -> self#f#env#mk_gloc_variable gloc offset)
12991305
(gloc#address_offset_memory_offset
13001306
~tgtsize:size ~tgtbtype:btype xoff)
@@ -1310,6 +1316,7 @@ object (self)
13101316
match memmap#xpr_containing_location addrvalue with
13111317
| Some gloc ->
13121318
(TR.tmap
1319+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
13131320
(fun offset -> self#f#env#mk_gloc_variable gloc offset)
13141321
(gloc#address_memory_offset ~tgtsize:size ~tgtbtype:btype addrvalue))
13151322
| _ ->
@@ -1320,56 +1327,116 @@ object (self)
13201327
self#f#env#mk_offset_memory_variable memref memoff)
13211328
memref_r memoff_r
13221329

1323-
method private get_variable_type (v: variable_t): btype_t option =
1330+
method private get_variable_type (v: variable_t): btype_t traceresult =
13241331
if self#f#env#is_initial_register_value v then
13251332
let reg_r = self#f#env#get_initial_register_value_register v in
1326-
TR.tfold_default
1333+
TR.tbind
1334+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
13271335
(fun reg ->
13281336
if self#f#get_summary#has_parameter_for_register reg then
13291337
let param = self#f#get_summary#get_parameter_for_register reg in
1330-
Some param.apar_type
1338+
Ok param.apar_type
13311339
else
1332-
self#env#get_variable_type v)
1333-
None
1340+
let ty = self#env#get_variable_type v in
1341+
match ty with
1342+
| None ->
1343+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1344+
^ "variable: " ^ (x2s (XVar v))]
1345+
| Some t -> Ok t)
13341346
reg_r
13351347
else if self#env#is_initial_memory_value v then
13361348
let memvar_r = self#env#get_init_value_variable v in
1337-
TR.tfold
1338-
~ok:self#get_variable_type
1339-
~error:(fun e ->
1340-
begin log_error_result __FILE__ __LINE__ e; None end)
1349+
TR.tbind
1350+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
1351+
self#get_variable_type
13411352
memvar_r
1353+
else if self#env#is_memory_variable v then
1354+
let memref_r = self#env#get_memory_reference v in
1355+
let memoff_r = self#env#get_memvar_offset v in
1356+
let basevar_r =
1357+
TR.tbind
1358+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
1359+
(fun memref ->
1360+
match memref#get_base with
1361+
| BaseVar v -> Ok v
1362+
| b ->
1363+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1364+
^ "memory-base: " ^ (p2s (memory_base_to_pretty b))])
1365+
memref_r in
1366+
let basevar_type_r =
1367+
TR.tbind
1368+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
1369+
self#get_variable_type
1370+
basevar_r in
1371+
TR.tbind
1372+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
1373+
(fun basevartype ->
1374+
TR.tbind
1375+
(fun memoff ->
1376+
match memoff with
1377+
| NoOffset when is_pointer basevartype ->
1378+
Ok (ptr_deref basevartype)
1379+
| ConstantOffset (n, NoOffset) when is_pointer basevartype ->
1380+
let symmemoff_r =
1381+
address_memory_offset
1382+
(ptr_deref basevartype) (num_constant_expr n) in
1383+
TR.tbind
1384+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1385+
^ "basevar type: " ^ (btype_to_string basevartype)
1386+
^ "; offset: " ^ n#toString)
1387+
(fun off ->
1388+
match off with
1389+
| FieldOffset ((fname, ckey), NoOffset) ->
1390+
let cinfo = get_compinfo_by_key ckey in
1391+
let finfo = get_compinfo_field cinfo fname in
1392+
Ok finfo.bftype
1393+
| _ ->
1394+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1395+
^ "symbolic offset: "
1396+
^ (memory_offset_to_string off)
1397+
^ " with basevar type: "
1398+
^ (btype_to_string basevartype)
1399+
^ " not yet handled"])
1400+
symmemoff_r
1401+
| _ ->
1402+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1403+
^ "memoff: " ^ (memory_offset_to_string memoff)
1404+
^ " not yet handled"])
1405+
memoff_r)
1406+
basevar_type_r
13421407
else
1343-
self#env#get_variable_type v
1408+
let ty = self#env#get_variable_type v in
1409+
match ty with
1410+
| None ->
1411+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1412+
^ "variable: " ^ (x2s (XVar v))]
1413+
| Some t -> Ok t
13441414

13451415
method convert_variable_offsets
13461416
?(size=None) (v: variable_t): variable_t traceresult =
13471417
if self#env#is_basevar_memory_variable v then
13481418
let basevar_r = self#env#get_memvar_basevar v in
13491419
let offset_r = self#env#get_memvar_offset v in
13501420
let cbasevar_r = TR.tbind self#convert_value_offsets basevar_r in
1351-
let basetype_r = TR.tmap self#get_variable_type cbasevar_r in
1421+
let basetype_r = TR.tbind self#get_variable_type cbasevar_r in
13521422
let tgttype_r =
13531423
TR.tbind
1424+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
13541425
(fun basetype ->
13551426
match basetype with
1356-
| Some (TPtr (t, _)) -> Ok t
1357-
| Some t ->
1427+
| TPtr (t, _) -> Ok t
1428+
| t ->
13581429
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
13591430
^ "Type " ^ (btype_to_string t)
1360-
^ " is not a pointer"]
1361-
| _ ->
1362-
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1363-
^ "No type for variable "
1364-
^ (p2s v#toPretty)
1365-
^ "with basevar "
1366-
^ (p2s (TR.tget_ok cbasevar_r)#toPretty)]) basetype_r in
1431+
^ " is not a pointer"]) basetype_r in
13671432
let coffset_r =
13681433
TR.tbind
1434+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
13691435
(fun offset ->
13701436
match offset with
13711437
| ConstantOffset (n, NoOffset) ->
13721438
TR.tbind
1439+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
13731440
(fun tgttype ->
13741441
address_memory_offset
13751442
~tgtsize:size tgttype (num_constant_expr n)) tgttype_r
@@ -1391,33 +1458,31 @@ object (self)
13911458
let basevar_r = self#env#get_memval_basevar v in
13921459
let offset_r = self#env#get_memval_offset v in
13931460
let cbasevar_r = TR.tbind self#convert_value_offsets basevar_r in
1394-
let basetype_r = TR.tmap self#get_variable_type cbasevar_r in
1461+
let basetype_r = TR.tbind self#get_variable_type cbasevar_r in
13951462
let tgttype_r =
13961463
TR.tbind
1464+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
13971465
(fun basetype ->
13981466
match basetype with
1399-
| Some (TPtr (t, _)) -> Ok t
1400-
| Some t ->
1467+
| TPtr (t, _) -> Ok t
1468+
| t ->
14011469
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
14021470
^ "Type " ^ (btype_to_string t)
1403-
^ " is not a pointer"]
1404-
| _ ->
1405-
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1406-
^ "No type for variable "
1407-
^ (p2s v#toPretty)
1408-
^ "with basevar "
1409-
^ (p2s (TR.tget_ok cbasevar_r)#toPretty)]) basetype_r in
1471+
^ " is not a pointer"]) basetype_r in
14101472
let coffset_r =
14111473
TR.tbind
1474+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
14121475
(fun offset ->
14131476
match offset with
14141477
| NoOffset ->
14151478
TR.tbind
1479+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
14161480
(fun tgttype ->
14171481
address_memory_offset
14181482
~tgtsize:size tgttype (int_constant_expr 0)) tgttype_r
14191483
| ConstantOffset (n, NoOffset) ->
14201484
TR.tbind
1485+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
14211486
(fun tgttype ->
14221487
address_memory_offset
14231488
~tgtsize:size tgttype (num_constant_expr n)) tgttype_r
@@ -1456,10 +1521,12 @@ object (self)
14561521
| _ -> Ok exp in
14571522
aux x
14581523

1459-
method get_xpr_type (x: xpr_t): btype_t option =
1524+
method get_xpr_type (x: xpr_t): btype_t traceresult =
14601525
match x with
14611526
| XVar v -> self#get_variable_type v
1462-
| _ -> None
1527+
| _ ->
1528+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1529+
^ "xpr: " ^ (x2s x)]
14631530

14641531
method decompose_memaddr (x: xpr_t):
14651532
(memory_reference_int traceresult * memory_offset_t traceresult) =
@@ -1468,15 +1535,39 @@ object (self)
14681535
let knownpointers = List.filter self#f#is_base_pointer vars in
14691536
match knownpointers with
14701537
(* one known pointer, must be the base *)
1538+
| [base] when self#f#env#is_initial_stackpointer_value base ->
1539+
let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
1540+
let memref_r = self#env#mk_base_variable_reference base in
1541+
let memoff_r = address_memory_offset t_unknown offset in
1542+
(memref_r, memoff_r)
1543+
14711544
| [base] ->
14721545
let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
14731546
let memref_r = self#env#mk_base_variable_reference base in
1474-
let vartype = self#env#get_variable_type base in
1475-
let vartype = match vartype with None -> t_unknown | Some t -> t in
1476-
let rvartype = TR.tvalue (resolve_type vartype) ~default:t_unknown in
1477-
let basetype =
1478-
if is_pointer rvartype then ptr_deref rvartype else t_unknown in
1479-
let memoff_r = address_memory_offset basetype offset in
1547+
let vartype_r = self#get_variable_type base in
1548+
let rvartype_r =
1549+
TR.tbind
1550+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
1551+
resolve_type
1552+
vartype_r in
1553+
let basetype_r =
1554+
TR.tbind
1555+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
1556+
(fun t ->
1557+
if is_pointer t then
1558+
Ok (ptr_deref t)
1559+
else
1560+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1561+
^ "x: " ^ (x2s x) ^ "; base: " ^ (x2s (XVar base))
1562+
^ "; offset: " ^ (x2s offset)])
1563+
rvartype_r in
1564+
let memoff_r =
1565+
TR.tbind
1566+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
1567+
^ "base pointer: " ^ (x2s (XVar base)))
1568+
(fun basetype -> address_memory_offset basetype offset)
1569+
basetype_r in
1570+
14801571
(*
14811572
(match offset with
14821573
| XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))

‎CodeHawk/CHB/bchlib/bCHLibTypes.mli‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5959,7 +5959,7 @@ class type floc_int =
59595959
-> xpr_t (** address value *)
59605960
-> variable_t traceresult
59615961

5962-
method get_xpr_type: xpr_t -> btype_t option
5962+
method get_xpr_type: xpr_t -> btype_t traceresult
59635963

59645964
(** {2 Predicates on variables}*)
59655965

‎CodeHawk/CHB/bchlib/bCHMemoryReference.ml‎

Lines changed: 18 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -204,7 +204,9 @@ let rec address_memory_offset
204204
arrayvar_memory_offset ~tgtsize ~tgtbtype rbasetype xoffset
205205
else
206206
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
207-
^ "Offset " ^ (x2s xoffset) ^ " not yet supported"]
207+
^ "Offset " ^ (x2s xoffset) ^ " with base type "
208+
^ (btype_to_string rbasetype)
209+
^ " not yet supported"]
208210

209211
and structvar_memory_offset
210212
~(tgtsize: int option)
@@ -226,9 +228,15 @@ and structvar_memory_offset
226228
^ " xoffset: " ^ (x2s xoffset)
227229
^ "; btype: " ^ (btype_to_string btype)]
228230
| _ ->
229-
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
230-
^ " xoffset: " ^ (x2s xoffset)
231-
^ "; btype: " ^ (btype_to_string btype)]
231+
if is_struct_type btype then
232+
let compinfo = get_struct_type_compinfo btype in
233+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
234+
^ "xoffset: " ^ (x2s xoffset)
235+
^ "; type: struct " ^ compinfo.bcname]
236+
else
237+
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
238+
^ "xoffset: " ^ (x2s xoffset)
239+
^ "; btype: " ^ (btype_to_string btype)]
232240

233241
and arrayvar_memory_offset
234242
~(tgtsize: int option)
@@ -250,6 +258,7 @@ and arrayvar_memory_offset
250258
if is_array_type btype then
251259
let eltty = get_element_type btype in
252260
TR.tbind
261+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
253262
(fun elsize ->
254263
let optindex = BCHXprUtil.get_array_index_offset xoffset elsize in
255264
match optindex with
@@ -265,10 +274,12 @@ and arrayvar_memory_offset
265274
if (TR.tfold_default is_struct_type false (resolve_type eltty)) then
266275
let eltty = TR.tvalue (resolve_type eltty) ~default:t_unknown in
267276
TR.tbind
277+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
268278
(fun suboff -> Ok (ArrayIndexOffset (indexxpr, suboff)))
269279
(structvar_memory_offset ~tgtsize ~tgtbtype eltty rem)
270280
else if is_array_type eltty then
271281
TR.tbind
282+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
272283
(fun suboff -> Ok (ArrayIndexOffset (indexxpr, suboff)))
273284
(arrayvar_memory_offset ~tgtsize ~tgtbtype eltty rem)
274285
else if is_scalar eltty then
@@ -341,6 +352,7 @@ and get_field_memory_offset_at
341352
else
342353
let offset = offset - foff in
343354
TR.tbind
355+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
344356
(fun fldtype ->
345357
if offset = 0
346358
&& (is_scalar fldtype)
@@ -354,6 +366,7 @@ and get_field_memory_offset_at
354366
^ (compliance_failure fldtype sz)]
355367
else if is_struct_type fldtype then
356368
TR.tmap
369+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
357370
(fun suboff ->
358371
Some (FieldOffset
359372
((finfo.bfname, finfo.bfckey), suboff)))
@@ -364,6 +377,7 @@ and get_field_memory_offset_at
364377
(int_constant_expr offset))
365378
else if is_array_type fldtype then
366379
TR.tmap
380+
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
367381
(fun suboff ->
368382
Some (FieldOffset
369383
((finfo.bfname, finfo.bfckey), suboff)))

‎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_20250308"
99-
~date:"2025-03-08"
98+
~version:"0.6.0_20250312"
99+
~date:"2025-03-12"
100100
~licensee: None
101101
~maxfilesize: None
102102
()

0 commit comments

Comments
 (0)