Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
5 changes: 5 additions & 0 deletions CodeHawk/CHB/bchcil/bCHParseCilFile.ml
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,11 @@ let parse_cil_file ?(computeCFG=true) ?(removeUnused=true) (filename: string) =
NL];
exit 1
end
| CHCommon.CHFailure p ->
begin
pr_debug [STR "Error when parsing "; STR filename; STR ": "; p; NL];
exit 1
end
| e ->
begin
pr_debug [STR "Error when parsing (other exception): "; STR filename; NL];
Expand Down
1 change: 1 addition & 0 deletions CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -891,6 +891,7 @@ let main () =
let _ =
if (List.length system_info#ifiles > 0) then
pr_timing [STR "c header files parsed"] in
let _ = BCHBCTypeXml.register_ch_named_struct_types () in
(* function annotations in userdata should be loaded after the header
files are parsed, so types in the function annotations can be resolved.*)
let _ = system_info#initialize_function_annotations in
Expand Down
39 changes: 38 additions & 1 deletion CodeHawk/CHB/bchlib/bCHBCFiles.ml
Original file line number Diff line number Diff line change
Expand Up @@ -97,14 +97,51 @@ object (self)
val vinfo_srcmap = H.create 3
(* varinfo.ix -> (ix(filename), linenr, binloc, [ix(notes)]) *)

val mutable varinfo_vid_counter = 10000
val mutable varinfo_vid_counter = 100000
val mutable compinfo_ckey_counter = 100000

method private get_varinfo_id =
begin
varinfo_vid_counter <- varinfo_vid_counter + 1;
varinfo_vid_counter
end

method private get_compinfo_ckey =
begin
compinfo_ckey_counter <- compinfo_ckey_counter + 1;
compinfo_ckey_counter
end

method add_ch_named_struct_type (name: string) =
if H.mem gtypes name then
()
else
let loc = {line = (-1); file = ""; byte = (-1)} in
let locix = bcd#index_location loc in
let structname = "_" ^ name ^ "_st" in
let ckey = self#get_compinfo_ckey in
let compinfo = {
bcstruct = true;
bcname = structname;
bckey = ckey;
bcfields = [];
bcattr = []
} in
let typeinfo = { btname = name; bttype = TComp (ckey, []) } in
begin
ignore (bcd#index_typeinfo typeinfo);
H.add gtypes name (bcd#index_typ typeinfo.bttype, locix);
H.replace
gcomptagdecls
(compinfo.bcname, compinfo.bckey)
(bcd#index_compinfo compinfo, locix);
log_result
~tag:"add_ch_named_struct_type"
~msg:name
__FILE__ __LINE__
[btype_to_string (typeinfo.bttype)]
end

method add_bcfile (f: bcfile_t) =
let i = bcd#index_location in

Expand Down
29 changes: 27 additions & 2 deletions CodeHawk/CHB/bchlib/bCHBCTypeXml.ml
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,14 @@ let raise_error (node: xml_element_int) (msg: pretty_t) =
end


let ch_named_struct_types = [
"ch_FILE"
]

let register_ch_named_struct_types () =
List.iter BCHBCFiles.bcfiles#add_ch_named_struct_type ch_named_struct_types


(* Convert some standard type names as used in the legacy summaries to
btype enumerations*)
let get_standard_txt_type (t: string): btype_t option =
Expand All @@ -76,9 +84,12 @@ let get_standard_txt_type (t: string): btype_t option =
| "Integer" -> Some (TInt (IInt, []))
| "long" -> Some (TInt (ILong, []))
| "LONG" -> Some (TInt (ILong, []))
| "off_t" -> Some (TInt (IULong, []))
| "OLECHAR" -> Some (TInt (IWChar, []))
| "size_t" -> Some (TInt (IUInt, []))
| "SIZE_T" -> Some (TInt (IUInt, []))
| "ssize_t" -> Some (TInt (ILong, []))
| "time_t" -> Some (TInt (ILong, []))
| "UINT" -> Some (TInt (IUInt, []))
| "uint16_t" -> Some (TInt (IUShort, []))
| "uint32_t" -> Some (TInt (IUInt, []))
Expand All @@ -88,8 +99,22 @@ let get_standard_txt_type (t: string): btype_t option =
| "VOID" -> Some (TVoid ([]))
| "wchar_t" -> Some (TInt (IWChar, []))
| _ ->
let _ = chlog#add "legacy type name" (STR t) in
None
if List.mem t ch_named_struct_types then
begin
log_result
~tag:"get_standard_txt_type:provided by typedef"
__FILE__ __LINE__
[t];
None
end
else
begin
log_result
~tag:"get_standard_txt_type:legacy type not covered"
__FILE__ __LINE__
[t];
None
end


let read_xml_summary_type (node: xml_element_int): btype_t =
Expand Down
3 changes: 3 additions & 0 deletions CodeHawk/CHB/bchlib/bCHBCTypeXml.mli
Original file line number Diff line number Diff line change
Expand Up @@ -45,3 +45,6 @@ val read_xml_returntype: xml_element_int -> btype_t
val read_xml_summary_struct: xml_element_int -> bcompinfo_t

val read_xml_type_transformer: xml_element_int -> type_transformer_t


val register_ch_named_struct_types: unit -> unit
2 changes: 2 additions & 0 deletions CodeHawk/CHB/bchlib/bCHBCTypes.mli
Original file line number Diff line number Diff line change
Expand Up @@ -518,6 +518,8 @@ class type bcfiles_int =
(** [add_bcfile f] adds a parsed file [f] to the storage.*)
method add_bcfile: bcfile_t -> unit

method add_ch_named_struct_type: string -> unit

(** [add_fundef name type] adds an otherwise constructed function
definition to the storage (i.e., not parsed).*)
method add_fundef: ?attrs:b_attributes_t -> string -> btype_t -> unit
Expand Down
14 changes: 14 additions & 0 deletions CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml
Original file line number Diff line number Diff line change
Expand Up @@ -375,4 +375,18 @@ let get_type_arg_mode
| _ -> None) None predicates
else
mode in
let mode =
if Option.is_none mode then
List.fold_left (fun acc p ->
match acc with
| Some _ -> acc
| _ ->
match p with
| XXFreed (ArgValue param)
when Option.is_some param.apar_index
&& (Option.get param.apar_index) = argindex ->
Some ArgDeallocate
| _ -> None) None predicates
else
mode in
mode
2 changes: 2 additions & 0 deletions CodeHawk/CHB/bchlib/bCHLibTypes.mli
Original file line number Diff line number Diff line change
Expand Up @@ -3244,6 +3244,7 @@ type type_arg_mode_t =
| ArgDerefReadWrite of int option
| ArgDerefRead of int option
| ArgDerefWrite of int option
| ArgDeallocate
| ArgFunctionPointer
| ArgScalarValue

Expand Down Expand Up @@ -3296,6 +3297,7 @@ type type_constant_t =
| TyTStruct of int * string (** bckey, bcname *)
| TyTFloat of fkind_t
| TyVoid (** only to be used in the context of a void pointer *)
| TyNamed of string
| TyTUnknown (** top in type lattice *)
| TyBottom (** bottom in type lattice *)

Expand Down
3 changes: 2 additions & 1 deletion CodeHawk/CHB/bchlib/bCHSideeffect.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

Copyright (c) 2005-2019 Kestrel Technology LLC
Copyright (c) 2020 Henny B. Sipma
Copyright (c) 2021-2025 Aarno Labs LLC
Copyright (c) 2021-2026 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
Expand Down Expand Up @@ -146,6 +146,7 @@ let read_xml_sideeffect
XXBlockWrite (get_type (arg 0), get_term (arg 1), get_term (arg 2))
(* | "allocates-stack-memory" -> AllocatesStackMemory (get_term (arg 0)) *)
| "modifies" -> XXModified (get_term (arg 0))
| "frees" -> XXFreed (get_term (arg 0))
| "starts-thread" ->
XXStartsThread (get_term (arg 0), List.map get_term (List.tl argNodes))
| "invalidates" -> XXInvalidated (get_term (arg 0))
Expand Down
8 changes: 5 additions & 3 deletions CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

Copyright (c) 2005-2020 Kestrel Technology LLC
Copyright (c) 2020 Henny Sipma
Copyrigth (c) 2021-2025 Aarno Labs LLC
Copyrigth (c) 2021-2026 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
Expand Down Expand Up @@ -528,10 +528,11 @@ object
| ArgDerefReadWrite _ -> "rw"
| ArgDerefRead _ -> "r"
| ArgDerefWrite _ -> "w"
| ArgDeallocate -> "d"
| ArgFunctionPointer -> "fp"
| ArgScalarValue -> "s"

method !tags = ["fp"; "r"; "rw"; "s"; "w"]
method !tags = ["d"; "fp"; "r"; "rw"; "s"; "w"]

end

Expand Down Expand Up @@ -611,11 +612,12 @@ object
| TyTStruct _ -> "ts"
| TyTFloat _ -> "tf"
| TyVoid -> "vp"
| TyNamed _ -> "n"
| TyTUnknown -> "u"
| TyBottom -> "b"

method !tags = [
"a"; "ac"; "acl"; "ap"; "asl"; "ax"; "b"; "i";
"a"; "ac"; "acl"; "ap"; "asl"; "ax"; "b"; "i"; "n";
"s"; "ti"; "tf"; "ts"; "u"; "vp"; "z"]

end
Expand Down
6 changes: 5 additions & 1 deletion CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,8 @@ object (self)
| ArgDerefReadWrite optsize
| ArgDerefRead optsize
| ArgDerefWrite optsize -> (tags, [index_opt optsize])
| ArgFunctionPointer
| ArgDeallocate
| ArgFunctionPointer
| ArgScalarValue -> (tags, []) in
type_arg_mode_table#add key

Expand All @@ -102,6 +103,7 @@ object (self)
let a = a name args in
let getsize () = if (a 0) = (-1) then None else Some (a 0) in
match (t 0) with
| "d" -> ArgDeallocate
| "fp" -> ArgFunctionPointer
| "r" -> ArgDerefRead (getsize ())
| "rw" -> ArgDerefReadWrite (getsize ())
Expand Down Expand Up @@ -215,6 +217,7 @@ object (self)
| TyTStruct (key, name) -> (tags @ [name], [key])
| TyTFloat k -> (tags @ [fkind_mfts#ts k], [])
| TyVoid -> (tags, [])
| TyNamed s -> (tags @ [s], [])
| TyBottom -> (tags, [])
| TyTUnknown -> (tags, []) in
type_constant_table#add key
Expand All @@ -236,6 +239,7 @@ object (self)
| "ti" -> TyTInt (signedness_mfts#fs (t 1), a 0)
| "tf" -> TyTFloat (fkind_mfts#fs (t 1))
| "ts" -> TyTStruct (a 0, t 1)
| "n" -> TyNamed (t 1)
| "vp" -> TyVoid
| "b" -> TyBottom
| "u" -> TyTUnknown
Expand Down
16 changes: 13 additions & 3 deletions CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
Original file line number Diff line number Diff line change
Expand Up @@ -660,6 +660,10 @@ object (self)
(List.map type_cap_label_to_string caps))])
vars) evaluation in
let result =
let promote (ty: btype_t): btype_t =
match ty with
| TInt _ -> BCHBCTypeUtil.promote_int ty
| _ -> ty in
H.fold (fun k v a ->
if v#isEmpty then
if k = "return" then
Expand All @@ -683,7 +687,10 @@ object (self)
match v#singleton with
| Some ixty ->
if k = "return" then
begin returnresult := Some (bcd#get_typ ixty); a end
begin
returnresult := Some (promote (bcd#get_typ ixty));
a
end
else
let optparamindex =
match k with
Expand All @@ -698,11 +705,14 @@ object (self)
if H.mem capresult k then
let caps = H.find capresult k in
List.flatten
(List.map (convert_function_capabilities_to_attributes index) caps)
(List.map
(convert_function_capabilities_to_attributes index)
caps)
else
[]
| _ -> [] in
(register_from_string k, Some (bcd#get_typ ixty), attrs) :: a
let regty = promote (bcd#get_typ ixty) in
(register_from_string k, Some regty, attrs) :: a
| _ ->
if k = "return" then
let _ =
Expand Down
17 changes: 16 additions & 1 deletion CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,9 @@ let _type_arg_mode_compare (m1: type_arg_mode_t) (m2: type_arg_mode_t): int =
optvalue_compare i1 i2 Stdlib.compare
| (ArgDerefWrite _, _) -> -1
| (_, ArgDerefWrite _) -> 1
| (ArgDeallocate, ArgDeallocate) -> 0
| (ArgDeallocate, _) -> -1
| (_, ArgDeallocate) -> 1
| (ArgFunctionPointer, ArgFunctionPointer) -> 0
| (ArgFunctionPointer, _) -> -1
| (_, ArgFunctionPointer) -> 1
Expand Down Expand Up @@ -139,6 +142,7 @@ let type_arg_mode_to_string (m: type_arg_mode_t) =
| ArgDerefReadWrite i -> "rw" ^ (optsize_to_string i)
| ArgDerefRead i -> "r" ^ (optsize_to_string i)
| ArgDerefWrite i -> "w" ^ (optsize_to_string i)
| ArgDeallocate -> "d"
| ArgFunctionPointer -> "fp"
| ArgScalarValue -> "sv"

Expand Down Expand Up @@ -223,6 +227,7 @@ let type_constant_to_string (c: type_constant_t) =
| TyTStruct (_, name) -> "t_struct_" ^ name
| TyTFloat k -> float_type_to_string k
| TyVoid -> "t_void"
| TyNamed name -> "t_named " ^ name
| TyTUnknown -> "t_top"
| TyBottom -> "t_bottom"

Expand Down Expand Up @@ -339,6 +344,9 @@ let join_tc (t1: type_constant_t) (t2: type_constant_t): type_constant_t =
| _ -> TyTUnknown)
| TyTInt _, _ -> t1
| _, TyTInt _ -> t2
| TyNamed s1, TyNamed s2 when s1 = s2 -> t1
| TyNamed _, _ -> TyTUnknown
| _, TyNamed _ -> TyTUnknown
| _, _ -> TyTInt (SignedNeutral, 8)


Expand Down Expand Up @@ -464,6 +472,7 @@ let convert_function_capabilities_to_attributes
| ArgDerefReadWrite _ -> "read_write"
| ArgDerefRead _ -> "read_only"
| ArgDerefWrite _ -> "write_only"
| ArgDeallocate -> "deallocate"
| ArgFunctionPointer -> "fp"
| ArgScalarValue -> "sv" in
let result = new CHUtils.IntCollections.set_t in
Expand All @@ -477,7 +486,7 @@ let convert_function_capabilities_to_attributes
AStr callsite;
AStr callee;
AInt argindex;
ACons (type_arg_mode_to_attr_string mode, [])]) in
AStr (type_arg_mode_to_attr_string mode)]) in
result#add (bcd#index_attribute attr)
| _ -> ()) caps in
List.map bcd#get_attribute result#toList
Expand Down Expand Up @@ -575,6 +584,8 @@ let rec mk_btype_constraint
end
| Ok ty ->
match ty with
| TNamed (s, _) ->
Some (TyGround (TyVariable tv, TyConstant (TyNamed s)))
| TInt (ikind, _) ->
let (signedness, size) = ikind_to_signedsize ikind in
Some (TyGround
Expand All @@ -587,6 +598,9 @@ let rec mk_btype_constraint
| TPtr (TVoid _, _) when use_voidptr ->
let ptv = add_deref_capability tv in
Some (TyGround (TyVariable ptv, TyConstant TyVoid))
| TPtr (TNamed (s, _), _) when use_voidptr ->
let ptv = add_deref_capability tv in
Some (TyGround (TyVariable ptv, TyConstant (TyNamed s)))
| TPtr (TVoid _, _) -> None
| TPtr (pty, _) ->
let ptv = add_deref_capability tv in
Expand Down Expand Up @@ -665,6 +679,7 @@ let type_constant_to_btype (tc: type_constant_t) =
| TyTStruct (key, _) -> get_compinfo_struct_type (bcfiles#get_compinfo key)
| TyTFloat fkind -> TFloat (fkind, FScalar, [])
| TyVoid -> t_void
| TyNamed s -> t_named s
| TyBottom -> t_unknown
| TyTUnknown -> t_unknown

Expand Down
4 changes: 2 additions & 2 deletions CodeHawk/CHB/bchlib/bCHVersion.ml
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_20260324"
~date:"2026-03-24"
~version:"0.6.0_20260329"
~date:"2026-03-29"
~licensee: None
~maxfilesize: None
()
Loading
Loading