Skip to content

Liftingsupport #188

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sipma merged 2 commits into from
Apr 18, 2025
Merged

Liftingsupport #188

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c19fae4
CHB:ARM: show global variables in assembly listing
sipma Apr 18, 2025
0122cb3
CHB: add more support for conversion to C expressions
sipma Apr 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 10 additions & 6 deletions CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,8 @@ open BCHNumericalConstraints
module H = Hashtbl
module TR = CHTraceResult

let p2s = CHPrettyUtil.pretty_to_string


module ConstraintCollections = CHCollections.Make
(struct
Expand Down Expand Up @@ -442,17 +444,19 @@ let extract_valuesets
H.iter (fun k v ->
if H.mem v "valuesets" then
let inv = H.find v "valuesets" in
let flocinv = finfo#finv#get_location_invariant k in
let domain = inv#getDomain "valuesets" in
let varObserver = domain#observer#getNonRelationalVariableObserver in
let vars = domain#observer#getObservedVariables in
let knownvars = flocinv#get_known_variables in
let vars =
List.filter (fun v ->
not (v#isTmp || List.mem v knownvars)) vars in
let vars = List.filter (fun v -> not v#isTmp) vars in
List.iter (fun (v:variable_t) ->
let valueset = (varObserver v)#toValueSet in
if valueset#isTop then () else
if valueset#isTop then
let _ =
log_diagnostics_result
~tag:"value-sets: top"
__FILE__ __LINE__ [k ^ ": " ^ (p2s v#toPretty)] in
()
else
if valueset#removeZeroOffset#isSingleBase then
let (base,offset) = valueset#removeZeroOffset#getSingleBase in
let canbenull:bool = valueset#includesZero in
Expand Down
52 changes: 51 additions & 1 deletion CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -195,10 +195,16 @@ object (self)
~(tgtbtype: btype_t option)
(c: bcompinfo_t)
(xoffset: xpr_t): memory_offset_t traceresult =
let is_void_tgtbtype =
match tgtbtype with
| Some (TVoid _) -> true
| _ -> false in
let check_tgttype_compliance (t: btype_t) (s: int) =
match tgtsize, tgtbtype with
| None, None -> true
| Some size, None -> size = s
| Some size, Some (TVoid _) -> size = s
| None, Some (TVoid _) -> true
| None, Some ty -> btype_equal ty t
| Some size, Some ty -> size = s && btype_equal ty t in
let compliance_failure (t: btype_t) (s: int) =
Expand Down Expand Up @@ -246,7 +252,10 @@ object (self)
let offset = offset - foff in
tbind
(fun fldtype ->
if offset = 0
if offset = 0 && is_void_tgtbtype then
Ok (Some (FieldOffset
((finfo.bfname, finfo.bfckey), NoOffset)))
else if offset = 0
&& (is_scalar fldtype)
&& (check_tgttype_compliance fldtype sz) then
Ok (Some (FieldOffset
Expand Down Expand Up @@ -305,6 +314,47 @@ object (self)
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
^ " xoffset: " ^ (x2s xoffset)
^ "; btype: " ^ (btype_to_string btype)]
| XOp (XPlus, [XOp (XMult, [XConst (IntConst n); XVar v]);
XConst (IntConst m)]) when is_struct_type btype ->
let compinfo = get_struct_type_compinfo btype in
let fldoffset = XConst (IntConst m) in
let memoffset_r =
self#get_field_memory_offset_at
~tgtsize:None ~tgtbtype:None compinfo fldoffset in
TR.tbind
(fun memoffset ->
match memoffset with
| FieldOffset ((fname, fckey), NoOffset) ->
let fcinfo = get_compinfo_by_key fckey in
let field = get_compinfo_field fcinfo fname in
let fieldtype = field.bftype in
if is_array_type fieldtype then
let eltype = get_element_type fieldtype in
let elsize_r = size_of_btype eltype in
TR.tbind
(fun elsize ->
if elsize = n#toInt then
let aoffset = ArrayIndexOffset (XVar v, NoOffset) in
let moffset =
BCHMemoryReference.add_offset memoffset aoffset in
Ok moffset
else
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
^ "field: " ^ fname
^ "; fieldtype: " ^ (btype_to_string fieldtype)
^ "; elementsize: " ^ (string_of_int elsize)
^ "; expected: " ^ n#toString])
elsize_r
else
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
^ "not an array type"]
| _ ->
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
^ "fldoffset: " ^ (x2s fldoffset)
^ "; memoffset: "
^ (BCHMemoryReference.memory_offset_to_string memoffset)])
memoffset_r

| _ ->
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
^ " xoffset: " ^ (x2s xoffset)
Expand Down
18 changes: 17 additions & 1 deletion CodeHawk/CHB/bchlib/bCHLocationInvariant.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,9 +58,13 @@ module H = Hashtbl
module TR = CHTraceResult


(* let x2p = XprToPretty.xpr_formatter#pr_expr *)
let x2p = XprToPretty.xpr_formatter#pr_expr
let tracked_locations = []

let p2s = CHPrettyUtil.pretty_to_string
let x2s x = p2s (x2p x)


let track_location loc p =
if List.mem loc tracked_locations then
chlog#add ("tracked:" ^ loc) p
Expand Down Expand Up @@ -1068,6 +1072,11 @@ object (self)
(self#get_location_invariant iaddr)#add_fact fact

method add_symbolic_expr_fact (iaddr:string) (v:variable_t) (x:xpr_t) =
let _ =
log_diagnostics_result
~tag:("add symbolic-expr fact for " ^ iaddr)
__FILE__ __LINE__
[(p2s v#toPretty) ^ ": " ^ (x2s x)] in
self#add iaddr (NonRelationalFact (v,FSymbolicExpr x))

method set_unreachable (iaddr:string) (domain:string) =
Expand All @@ -1091,6 +1100,13 @@ object (self)
(base:symbol_t)
(i:interval_t)
(canbenull:bool) =
let _ =
log_diagnostics_result
~tag:("add valueset fact for " ^ iaddr)
__FILE__ __LINE__
[(p2s v#toPretty) ^ ": "
^ "base: " ^ (p2s base#toPretty)
^ "; offset: " ^ (p2s i#toPretty)] in
let fact =
if i#isBottom then
Unreachable "valuesets"
Expand Down
4 changes: 2 additions & 2 deletions CodeHawk/CHB/bchlib/bCHVersion.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,8 +95,8 @@ end


let version = new version_info_t
~version:"0.6.0_20250401"
~date:"2025-04-01"
~version:"0.6.0_20250417"
~date:"2025-04-17"
~licensee: None
~maxfilesize: None
()
82 changes: 72 additions & 10 deletions CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@
============================================================================= *)

(* chlib *)
open CHNumerical
open CHPretty

(* chutil *)
Expand All @@ -34,8 +35,13 @@ open CHPrettyUtil
open CHTraceResult
open CHXmlDocument

(* xprlib *)
open Xprt
open XprTypes

(* bchlib *)
open BCHBasicTypes
open BCHBCTypePretty
open BCHByteUtilities
open BCHDataBlock
open BCHDoubleword
Expand All @@ -61,6 +67,9 @@ open BCHDisassembleThumbInstruction
module H = Hashtbl
module TR = CHTraceResult

let x2p = XprToPretty.xpr_formatter#pr_expr
let p2s = CHPrettyUtil.pretty_to_string
let x2s x = p2s (x2p x)

let numArrays = 1000
let arrayLength = 100000
Expand Down Expand Up @@ -676,6 +685,67 @@ object (self)
^ " String:<"
^ (fixed_length_string v#to_hex_string 12)
^ "> ... (cont'd)"

else if Option.is_some (memorymap#containing_location a) then
match memorymap#containing_location a with
| None -> ""
| Some gloc ->
let xprv = num_constant_expr a#to_numerical in
let offset_r = gloc#address_offset xprv in
TR.tfold_default
(fun offset ->
match offset with
| XConst (IntConst n) when n#equal numerical_zero ->
" "
^ (fixed_length_string addr 10)
^ " Global variable:<"
^ gloc#name
^ ": "
^ (btype_to_string gloc#btype)
^ ">"
^ "\n "
^ (fixed_length_string addr 10)
^ " GV:<"
^ gloc#name
^ ":0 >: "
^ v#to_hex_string
| XConst (IntConst n) ->
" "
^ (fixed_length_string addr 10)
^ " GV:<"
^ gloc#name
^ ":"
^ (fixed_length_string n#toString 3)
^ ">: "
^ v#to_hex_string
| _ ->
" "
^ (fixed_length_string addr 10)
^ " GV:<"
^ gloc#name
^ ":"
^ (x2s offset)
^ ">: "
^ v#to_hex_string)
(" "
^ (fixed_length_string addr 10)
^ " GV:<"
^ gloc#name
^ ":?>: "
^ v#to_hex_string)
offset_r

else if memorymap#has_elf_symbol v then
let name = memorymap#get_elf_symbol v in
" "
^ (fixed_length_string addr 10)
^ " Sym:<"
^ v#to_hex_string
^ ":"
^ name
^ ">"
^ datarefstr

else if v#equal wordzero then
" "
^ (fixed_length_string addr 10)
Expand All @@ -684,6 +754,7 @@ object (self)
" "
^ (fixed_length_string addr 10)
^ " <0xffffffff>"

else if functions_data#is_function_entry_point v then
let name =
if functions_data#has_function_name v then
Expand All @@ -698,16 +769,7 @@ object (self)
^ name
^ ">"
^ datarefstr
else if memorymap#has_elf_symbol v then
let name = memorymap#get_elf_symbol v in
" "
^ (fixed_length_string addr 10)
^ " Sym:<"
^ v#to_hex_string
^ ":"
^ name
^ ">"
^ datarefstr

else if elf_header#is_code_address v then
" "
^ (fixed_length_string addr 10)
Expand Down
34 changes: 20 additions & 14 deletions CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -649,9 +649,11 @@ object (self)
match xx with
| XVar _ -> xx
| _ ->
TR.tfold_default
(fun v -> XOp ((Xf "addressofvar"), [(XVar v)]))
xx
TR.tfold
~ok:(fun v -> XOp ((Xf "addressofvar"), [(XVar v)]))
~error:(fun e ->
let _ = log_dc_error_result __FILE__ __LINE__ e in
xx)
(floc#get_var_at_address ~btype:(ptr_deref ptype) xx)
else
xx in
Expand Down Expand Up @@ -770,21 +772,23 @@ object (self)
let xrm_r = rm#to_expr floc in
let result_r =
TR.tmap2 (fun xrn xrm -> XOp (XPlus, [xrn; xrm])) xrn_r xrm_r in
let xxrn_r = TR.tmap rewrite_expr xrn_r in
let xxrm_r = TR.tmap rewrite_expr xrm_r in
let rresult_r = TR.tmap rewrite_expr result_r in
let cresult_r =
TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
let _ =
TR.tfold_default
(fun r -> ignore (get_string_reference floc r)) () rresult_r in
let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r] in
let uses = get_def_use_r vrd_r in
let useshigh = get_def_use_high_r vrd_r in
let rdefs =
[get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in
let uses = [get_def_use_r vrd_r] in
let useshigh = [get_def_use_high_r vrd_r] in
let vars_r = [vrd_r] in
let xprs_r = [xrn_r; xrm_r; result_r; rresult_r; xxrn_r; xxrm_r] in
let cxprs_r = [cresult_r] in
let (tagstring, args) =
mk_instrx_data_r
~vars_r:[vrd_r]
~xprs_r:[xrn_r; xrm_r; result_r; rresult_r]
~rdefs:rdefs
~uses:[uses]
~useshigh:[useshigh]
() in
mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
let (tags, args) = add_optional_instr_condition tagstring args c in
(tags, args)

Expand Down Expand Up @@ -2285,6 +2289,8 @@ object (self)
let xrm_r = rm#to_expr floc in
let result_r =
TR.tmap2 (fun xrn xrm -> XOp (XMinus, [xrm; xrn])) xrn_r xrm_r in
let xxrn_r = TR.tmap rewrite_expr xrn_r in
let xxrm_r = TR.tmap rewrite_expr xrm_r in
let rresult_r = TR.tmap rewrite_expr result_r in
let cresult_r =
TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in
Expand All @@ -2293,7 +2299,7 @@ object (self)
let uses = [get_def_use_r vrd_r] in
let useshigh = [get_def_use_high_r vrd_r] in
let vars_r = [vrd_r] in
let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in
let xprs_r = [xrn_r; xrm_r; result_r; rresult_r; xxrn_r; xxrm_r] in
let cxprs_r = [cresult_r] in
let (tagstring, args) =
mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in
Expand Down
5 changes: 4 additions & 1 deletion CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2345,7 +2345,10 @@ let translate_arm_instruction
if rl#includes_pc then
match rtype with
| TVoid _ -> []
| _ -> [floc#f#env#mk_arm_register_variable AR0]
| _ ->
let r0_op = arm_register_op AR0 RD in
let xr0 = r0_op#to_expr floc in
get_use_high_vars_r [xr0]
else
[] in
let popdefcmds =
Expand Down