From bd45769bbe40e25f355d1194052581b4f54db36f Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 16 Mar 2025 11:11:00 -0700 Subject: [PATCH 1/5] CHB:VARINV: filter fact comparison based on variable index --- CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml b/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml index f7c9f504..7c72b851 100644 --- a/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml +++ b/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2022-2024 Aarno Labs LLC + Copyright (c) 2022-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -197,11 +197,13 @@ object (self) H.iter (fun _ (var, locs) -> let locs = List.sort Stdlib.compare locs#toList in - self#add_fact (DefUseHigh (var,locs))) usehighlocs + self#add_fact (DefUseHigh (var, locs))) usehighlocs end method get_var_facts (var: variable_t): var_invariant_int list = - List.filter (fun f -> f#get_variable#equal var) self#get_facts + let varix = var#getName#getSeqNumber in + List.filter (fun f -> + f#get_variable#getName#getSeqNumber = varix) self#get_facts method get_var_reaching_defs (var: variable_t): var_invariant_int list = List.filter (fun f -> f#is_reaching_def) (self#get_var_facts var) From b0b214b276a6491a53b48785ddcb92cd7319f894 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 16 Mar 2025 11:12:00 -0700 Subject: [PATCH 2/5] CHB: delay type-based variable representation conversion --- CodeHawk/CHB/bchlib/bCHFloc.ml | 31 ++++++++++++++++++++++++------- CodeHawk/CHB/bchlib/bCHVersion.ml | 2 +- 2 files changed, 25 insertions(+), 8 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index e7ab60e0..181f385c 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -699,17 +699,23 @@ object (self) let memoffset = numoffset#add offset in let memref_r = self#env#mk_base_sym_reference base in let memoff_r = + address_memory_offset + t_unknown ~tgtsize:(Some size) (num_constant_expr memoffset) in + (* + To keep representation unifor (i.e., to avoid aliasing) the creation + of variable representation against the type of the variable must be + delayed until reporting time. TR.tbind ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) (fun basevar -> let optbasetype = self#env#get_variable_type basevar in - let basetype = + let basetype = t_unknown in match optbasetype with | Some t when is_pointer t -> ptr_deref t | _ -> t_unknown in - address_memory_offset basetype + address_memory_offset t_unknown ~tgtsize:(Some size) (num_constant_expr memoffset)) - (self#env#get_variable base#getSeqNumber) in + (self#env#get_variable base#getSeqNumber) in *) mk_memvar memref_r memoff_r else @@ -1527,9 +1533,16 @@ object (self) ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) (fun v -> XVar v) (self#convert_variable_offsets ~size v) | XOp ((Xf "addressofvar"), [XVar v]) -> + let newx_r = + TR.tmap + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (fun v -> XVar v) (self#convert_variable_offsets ~size v) in TR.tmap - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (fun v -> XVar v) (self#convert_variable_offsets ~size v) + (fun newx -> + match newx with + | XVar v -> XOp ((Xf "addressofvar"), [(XVar v)]) + | _ -> exp) + newx_r | XOp (op, [xx]) -> TR.tmap (fun x -> XOp (op, [x])) (aux xx) | XOp (op, [x1; x2]) -> TR.tmap2 (fun x1 x2 -> XOp (op, [x1; x2])) (aux x1) (aux x2) @@ -1550,12 +1563,15 @@ object (self) let knownpointers = List.filter self#f#is_base_pointer vars in match knownpointers with (* one known pointer, must be the base *) - | [base] when self#f#env#is_initial_stackpointer_value base -> + | [base] (* when self#f#env#is_initial_stackpointer_value base *) -> let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in let memref_r = self#env#mk_base_variable_reference base in let memoff_r = address_memory_offset t_unknown offset in (memref_r, memoff_r) + (* resolving to type-based representations at this point may give + rise to aliasing; for example __ptr_deref_R[0]_in.field_4 may be aliased + with R[0]_in[4]_in | [base] -> let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in let memref_r = self#env#mk_base_variable_reference base in @@ -1582,6 +1598,7 @@ object (self) ^ "base pointer: " ^ (x2s (XVar base))) (fun basetype -> address_memory_offset basetype offset) basetype_r in + *) (* (match offset with @@ -1593,7 +1610,7 @@ object (self) ^ "Offset from base " ^ (x2s (XVar base)) ^ " not recognized: " ^ (x2s offset)]) in *) - (memref_r, memoff_r) + (* (memref_r, memoff_r) *) (* no known pointers, have to find a base *) | [] -> diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 9f44e67d..0dc5da81 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,7 +95,7 @@ end let version = new version_info_t - ~version:"0.6.0_20250314" + ~version:"0.6.0_20250316" ~date:"2025-03-14" ~licensee: None ~maxfilesize: None From 424da0d3c13a093f91dc5c1773241dd975e10712 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 16 Mar 2025 11:13:15 -0700 Subject: [PATCH 3/5] CHB:ARM: add special case for -1 in type assignment --- CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index 5a5b1f33..fd484f65 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -144,6 +144,7 @@ object (self) if i < 128 then (SignedNeutral, 8) else if i < BCHDoubleword.e15 then (SignedNeutral, 16) else if i < BCHDoubleword.e31 then (SignedNeutral, 32) + else if i = 0xffffffff then (Signed, 32) else (SignedNeutral, 64) in TyTInt (sg, si) in From 1de40b9fc394338824788245ebe26e66979192b9 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 16 Mar 2025 11:14:49 -0700 Subject: [PATCH 4/5] CHB:ARM: add LHS type-conversion for STRD --- CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 3b15a055..f09d8c9d 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -2757,7 +2757,13 @@ object (self) | StoreRegisterDual (c, rt, rt2, rn, rm, mem, mem2) -> let vmem_r = mem#to_variable floc in + let vmem_r = + let r = TR.tbind (floc#convert_variable_offsets ~size:(Some 4)) vmem_r in + if Result.is_ok r then r else vmem_r in let vmem2_r = mem2#to_variable floc in + let vmem2_r = + let r = TR.tbind (floc#convert_variable_offsets ~size:(Some 4)) vmem2_r in + if Result.is_ok r then r else vmem2_r in let xaddr1_r = mem#to_address floc in let xaddr2_r = mem2#to_address floc in let xaddr1_r = TR.tmap rewrite_expr xaddr1_r in From 025b0a1832e065c50c082b6c8d97122ff17b9ab7 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Mon, 17 Mar 2025 11:24:31 -0700 Subject: [PATCH 5/5] CHB:ARM: convert STMIB LHS to type-based representation --- CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index f09d8c9d..0114cd90 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -2631,6 +2631,11 @@ object (self) (fun (acc, off) _reg -> let memop = arm_reg_deref ~with_offset:off basereg WR in let memlhs_r = memop#to_variable floc in + let memlhs_r = + let r = + TR.tbind + (floc#convert_variable_offsets ~size:(Some 4)) memlhs_r in + if Result.is_ok r then r else memlhs_r in (acc @ [memlhs_r], off + 4)) ([], 4) rl#get_register_op_list in let rdefs = List.map get_rdef_r (baserhs_r :: rrhss_rl) in let uses = List.map get_def_use_r (baselhs_r :: memlhss_rl) in