diff --git a/CodeHawk/CHB/bchcmdline/Makefile b/CodeHawk/CHB/bchcmdline/Makefile index 67af13cf..adea39f1 100644 --- a/CodeHawk/CHB/bchcmdline/Makefile +++ b/CodeHawk/CHB/bchcmdline/Makefile @@ -84,8 +84,8 @@ defs: make_dirs libsum appsum constsum classsum structdef chx86_analyze: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CIL)/goblintCil.cmxa $(ZIPLIB)/zip.cmxa $(CHUTIL)/chutil.cmxa $(BCHCIL)/bchcil.cmxa $(BCHLIB)/bchlib.cmxa $(PELIB)/bchlibpe.cmxa $(X86LIB)/bchlibx86.cmxa $(MIPSLIB)/bchlibmips32.cmxa $(ARMLIB)/bchlibarm32.cmxa $(PWRLIB)/bchlibpower32.cmxa $(ANALYZ)/bchanalyze.cmxa cmi/bCHXBinaryAnalyzer.cmi cmx/bCHXBinaryAnalyzer.cmx $(CAMLLINK) -o $@ cmx/bCHXBinaryAnalyzer.cmx -chx86_inspect_summaries: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(ZIPLIB)/zip.cmxa $(CHUTIL)/chutil.cmxa $(BCHLIB)/bchlib.cmxa cmi/bCHXInspectSummaries.cmi cmx/bCHXInspectSummaries.cmx - $(CAMLLINK) -o $@ $(OBJECTS) cmx/bCHXInspectSummaries.cmx +chx86_inspect_summaries: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CIL)/goblintCil.cmxa $(ZIPLIB)/zip.cmxa $(CHUTIL)/chutil.cmxa $(BCHCIL)/bchcil.cmxa $(BCHLIB)/bchlib.cmxa cmi/bCHXInspectSummaries.cmi cmx/bCHXInspectSummaries.cmx + $(CAMLLINK) -o $@ cmx/bCHXInspectSummaries.cmx chx86_save_exports: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(ZIPLIB)/zip.cmxa $(CHUTIL)/chutil.cmxa $(BCHLIB)/bchlib.cmxa $(PELIB)/bchlibpe.cmxa cmx/bCHXSaveExports.cmx $(CAMLLINK) -o $@ $(OBJECTS) cmx/bCHXSaveExports.cmx diff --git a/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml b/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml index ff8e47a5..51ca4bb9 100644 --- a/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml +++ b/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml @@ -558,6 +558,7 @@ let main () = let _ = disassembly_summary#set_disassembly_metrics (get_arm_disassembly_metrics ()) in let _ = pr_debug [NL; NL; disassembly_summary#toPretty; NL] in + let _ = save_bc_files () in (* let _ = pr_debug [ diff --git a/CodeHawk/CHB/bchlib/Makefile b/CodeHawk/CHB/bchlib/Makefile index 9540d089..35e1c8e0 100644 --- a/CodeHawk/CHB/bchlib/Makefile +++ b/CodeHawk/CHB/bchlib/Makefile @@ -23,6 +23,7 @@ OCAMLDEP := ocamldep MLIS := \ bCHBCTypes \ + bCHBCAttributes \ bCHBCSumTypeSerializer \ bCHBCTypeTransformer \ bCHLibTypes \ @@ -41,7 +42,6 @@ MLIS := \ bCHBCFunDeclarations \ bCHBCWriteXml \ bCHBCFiles \ - bCHBCAttributes \ bCHInterfaceDictionary \ bCHVarDictionary \ bCHInvDictionary \ @@ -131,10 +131,10 @@ SOURCES := \ bCHBCDictionary \ bCHBCFunDeclarations \ bCHBCWriteXml \ + bCHBCAttributes \ bCHBCFiles \ bCHBCTypeUtil \ bCHBCTypeXml \ - bCHBCAttributes \ bCHSumTypeSerializer \ bCHDictionary \ bCHInterfaceDictionary \ diff --git a/CodeHawk/CHB/bchlib/bCHBCAttributes.ml b/CodeHawk/CHB/bchlib/bCHBCAttributes.ml index fa8ac693..24a6c3f7 100644 --- a/CodeHawk/CHB/bchlib/bCHBCAttributes.ml +++ b/CodeHawk/CHB/bchlib/bCHBCAttributes.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2024 Aarno Labs LLC + Copyright (c) 2024-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 @@ -50,6 +50,40 @@ let gcc_attributes_to_precondition_attributes | _ -> acc) [] attrs +let gcc_attributes_to_srcmapinfo + (attrs: b_attributes_t): srcmapinfo_t option = + let optsrcloc = + List.fold_left (fun acc a -> + match acc with + | Some _ -> acc + | _ -> + match a with + | Attr ("chkc_srcloc", params) -> + (match params with + | [AStr filename; AInt linenumber] -> + Some {srcloc_filename=filename; + srcloc_linenumber=linenumber; + srcloc_notes=[]} + | _ -> None) + | _ -> None) None attrs in + match optsrcloc with + | Some srcloc -> + let binloc = + List.fold_left (fun acc a -> + match acc with + | Some _ -> acc + | _ -> + match a with + | Attr ("chkx_binloc", params) -> + (match params with + | [AStr address] -> Some address + | _ -> None) + | _ -> None) None attrs in + Some {srcmap_srcloc = srcloc; srcmap_binloc = binloc} + | _ -> None + + + let precondition_attributes_t_to_gcc_attributes (preattrs: precondition_attribute_t list): b_attributes_t = let get_params (refindex: int) (optsizeindex: int option) = @@ -67,8 +101,3 @@ let precondition_attributes_t_to_gcc_attributes | APCReadWrite (refindex, optsizeindex) -> (get_access "read_write" (get_params refindex optsizeindex)) :: acc | _ -> acc) [] preattrs - - - - - diff --git a/CodeHawk/CHB/bchlib/bCHBCAttributes.mli b/CodeHawk/CHB/bchlib/bCHBCAttributes.mli index 322af470..c8e94a5b 100644 --- a/CodeHawk/CHB/bchlib/bCHBCAttributes.mli +++ b/CodeHawk/CHB/bchlib/bCHBCAttributes.mli @@ -31,6 +31,9 @@ open BCHBCTypes val gcc_attributes_to_precondition_attributes: b_attributes_t -> precondition_attribute_t list +val gcc_attributes_to_srcmapinfo: + b_attributes_t -> srcmapinfo_t option + val precondition_attributes_t_to_gcc_attributes: precondition_attribute_t list -> b_attributes_t diff --git a/CodeHawk/CHB/bchlib/bCHBCFiles.ml b/CodeHawk/CHB/bchlib/bCHBCFiles.ml index feeb1203..8a333a90 100644 --- a/CodeHawk/CHB/bchlib/bCHBCFiles.ml +++ b/CodeHawk/CHB/bchlib/bCHBCFiles.ml @@ -3,7 +3,7 @@ Author: Henny Sipma ------------------------------------------------------------------------------ The MIT License (MIT) - + Copyright (c) 2021-2024 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy @@ -12,10 +12,10 @@ to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: - + The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. - + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE @@ -60,6 +60,9 @@ object (self) val gvardecls = H.create 3 (* bvname -> (varinfo.ix, loc.ix) *) val gvars = H.create 3 (* idem *) val gfuns = H.create 3 (* bsvar.bvname -> (fundec, loc.ix) *) + val vinfo_srcmap = H.create 3 + (* varinfo.ix -> (ix(filename), linenr, binloc, [ix(notes)]) *) + val mutable varinfo_vid_counter = 10000 method private get_varinfo_id = @@ -70,6 +73,24 @@ object (self) method add_bcfile (f: bcfile_t) = let i = bcd#index_location in + + let add_srcmapinfo (vinfo: bvarinfo_t) = + match BCHBCAttributes.gcc_attributes_to_srcmapinfo vinfo.bvattr with + | Some srcmap -> + let vix = bcd#index_varinfo vinfo in + if H.mem vinfo_srcmap vix then + () + else + let srcloc = srcmap.srcmap_srcloc in + let ixfilename = bcd#index_string srcloc.srcloc_filename in + let linenumber = srcloc.srcloc_linenumber in + let ixnotes = List.map bcd#index_string srcloc.srcloc_notes in + let binloc = + match srcmap.srcmap_binloc with + | Some s -> s + | _ -> "none" in + H.add vinfo_srcmap vix (ixfilename, linenumber, binloc, ixnotes) + | _ -> () in begin List.iter (fun g -> match g with @@ -100,8 +121,10 @@ object (self) () else let _ = chlog#add "bcfiles:add gvardecl" (STR vinfo.bvname) in + let _ = add_srcmapinfo vinfo in H.replace gvardecls vinfo.bvname (bcd#index_varinfo vinfo, i loc) | GVar (vinfo, iinfo, loc) -> + let _ = add_srcmapinfo vinfo in let _ = chlog#add "bcfiles:add gvar" (STR vinfo.bvname) in H.replace gvars vinfo.bvname @@ -112,7 +135,7 @@ object (self) i loc) | GFun (fundec, loc) -> let _ = chlog#add "bcfiles:add gfun" (STR fundec.bsvar.bvname) in - H.replace gfuns fundec.bsvar.bvname (fundec, bcd#index_location loc); + H.replace gfuns fundec.bsvar.bvname (fundec, bcd#index_location loc); | _ -> ()) f.bglobals; chlog#add "bcfiles:add_bcfile" @@ -411,7 +434,7 @@ object (self) result := (v2s (bcd#get_varinfo ix)) :: !result) gvardecls; !result end - + method has_gfun (name: string) = H.mem gfuns name method get_gfun (name: string) = @@ -495,7 +518,7 @@ object (self) match cn#getIntListAttribute "ixs" with | [cix; locix] -> H.add gcomptags (name, ckey) (cix, locix) | _ -> ()) (getcc "cid") - + method private write_xml_genums (node: xml_element_int) = let genums = H.fold (fun k v a -> (k, v)::a) genumtags [] in node#appendChildren @@ -533,7 +556,7 @@ object (self) match en#getIntListAttribute "ixs" with | [eix; locix] -> H.add genumtagdecls name (eix, locix) | _ -> ()) (getcc "eid") - + method private write_xml_gvars (node: xml_element_int) = let gvarinfos = H.fold (fun k v a -> (k, v)::a) gvars [] in node#appendChildren @@ -591,7 +614,29 @@ object (self) let locix = gn#getIntAttribute "locix" in let fundec = read_xml_function_definition gn in H.add gfuns name (fundec, locix)) (getcc "gfun") - + + method private write_xml_srcmap (node: xml_element_int) = + let srcmapentries = H.fold (fun k v a -> (k, v)::a) vinfo_srcmap [] in + node#appendChildren + (List.map (fun (vix, (ixfn, lnr, binloc, _ixnotes)) -> + let snode = xmlElement "srcloc" in + begin + snode#setIntAttribute "vix" vix; + snode#setIntAttribute "ixfn" ixfn; + snode#setIntAttribute "lnr" lnr; + snode#setAttribute "binloc" binloc; + snode + end) srcmapentries) + + method private read_xml_srcmap (node: xml_element_int) = + let getcc = node#getTaggedChildren in + List.iter (fun gs -> + let vix = gs#getIntAttribute "vix" in + let ixfn = gs#getIntAttribute "ixfn" in + let lnr = gs#getIntAttribute "lnr" in + let binloc = gs#getAttribute "binloc" in + H.add vinfo_srcmap vix (ixfn, lnr, binloc, [])) (getcc "srcloc") + method write_xml (node: xml_element_int) = let tnode = xmlElement "typeinfos" in let cnode = xmlElement "compinfos" in @@ -601,6 +646,7 @@ object (self) let vnode = xmlElement "varinfos" in let vdnode = xmlElement "varinfodecls" in let gfunnode = xmlElement "gfuns" in + let srcmapnode = xmlElement "srcmap" in begin self#write_xml_gtypes tnode; self#write_xml_gcomps cnode; @@ -610,8 +656,9 @@ object (self) self#write_xml_gvars vnode; self#write_xml_gvardecls vdnode; self#write_xml_gfuns gfunnode; + self#write_xml_srcmap srcmapnode; node#appendChildren[ - tnode; cnode; cdnode; enode; ednode; vnode; vdnode; gfunnode] + tnode; cnode; cdnode; enode; ednode; vnode; vdnode; gfunnode; srcmapnode] end method read_xml (node: xml_element_int) = @@ -624,9 +671,10 @@ object (self) self#read_xml_genumdecls (getc "enuminfodecls"); self#read_xml_gvars (getc "varinfos"); self#read_xml_gvardecls (getc "varinfodecls"); - self#read_xml_gfuns (getc "gfuns") + self#read_xml_gfuns (getc "gfuns"); + self#read_xml_srcmap (getc "srcmap") end - + end diff --git a/CodeHawk/CHB/bchlib/bCHBCTypes.mli b/CodeHawk/CHB/bchlib/bCHBCTypes.mli index 73a6b66c..b143f4ca 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHBCTypes.mli @@ -419,6 +419,19 @@ type bcfile_t = { } +type srclocinfo_t = { + srcloc_filename: string; + srcloc_linenumber: int; + srcloc_notes: string list + } + + +type srcmapinfo_t = { + srcmap_srcloc: srclocinfo_t; + srcmap_binloc: string option + } + + class type bcdictionary_int = object diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 51c171cb..99ecfc29 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20250502" - ~date:"2025-05-02" + ~version:"0.6.0_20250521" + ~date:"2025-05-21" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml index 660a750a..352c77c0 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml @@ -357,9 +357,21 @@ object (self:'a) let xoffset = int_constant_expr indexoffset in (match srt with | ARMImmSRT (_, 0)-> Ok (XOp (XPlus, [XVar indexvar; xoffset])) + | ARMImmSRT (SRType_LSL, 1) -> + let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 2]) in + Ok (XOp (XPlus, [shifted; xoffset])) | ARMImmSRT (SRType_LSL, 2) -> let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 4]) in Ok (XOp (XPlus, [shifted; xoffset])) + | ARMImmSRT (SRType_LSL, 3) -> + let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 8]) in + Ok (XOp (XPlus, [shifted; xoffset])) + | ARMImmSRT (SRType_LSL, 4) -> + let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 16]) in + Ok (XOp (XPlus, [shifted; xoffset])) + | ARMImmSRT (SRType_LSL, 5) -> + let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 32]) in + Ok (XOp (XPlus, [shifted; xoffset])) | ARMImmSRT (SRType_ASR, 1) -> let shifted = XOp (XDiv, [XVar indexvar; int_constant_expr 2]) in Ok (XOp (XPlus, [shifted; xoffset])) @@ -369,6 +381,9 @@ object (self:'a) | ARMImmSRT (SRType_ASR, 3) -> let shifted = XOp (XDiv, [XVar indexvar; int_constant_expr 8]) in Ok (XOp (XPlus, [shifted; xoffset])) + | ARMImmSRT (SRType_ASR, 4) -> + let shifted = XOp (XDiv, [XVar indexvar; int_constant_expr 16]) in + Ok (XOp (XPlus, [shifted; xoffset])) | ARMRegSRT (SRType_LSL, srtreg) -> let shiftvar = env#mk_arm_register_variable srtreg in let shifted = XOp (XLsl, [XVar indexvar; XVar shiftvar]) in diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index cb4fd523..8534f970 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -2377,16 +2377,16 @@ object (self) (tags, args) | SignedBitFieldExtract (c, rd, rn) -> - let lhs_r = rd#to_variable floc in - let rhs_r = rn#to_expr floc in - let rrhs_r = TR.tmap rewrite_expr rhs_r in - let rdefs = [get_rdef_r rhs_r] in - let uses = [get_def_use_r lhs_r] in - let useshigh = [get_def_use_high_r lhs_r] in + let vrd_r = rd#to_variable floc in + let xrn_r = rn#to_expr floc in + let xxrn_r = TR.tmap rewrite_expr xrn_r in + let rdefs = [get_rdef_r xrn_r] in + let uses = [get_def_use_r vrd_r] in + let useshigh = [get_def_use_high_r vrd_r] in let (tagstring, args) = mk_instrx_data_r - ~vars_r:[lhs_r] - ~xprs_r:[rhs_r; rrhs_r] + ~vars_r:[vrd_r] + ~xprs_r:[xrn_r; xxrn_r] ~rdefs ~uses ~useshigh diff --git a/CodeHawk/CHC/cchlib/cCHCAttributes.ml b/CodeHawk/CHC/cchlib/cCHCAttributes.ml index 1a2fa46d..5aaf554a 100644 --- a/CodeHawk/CHC/cchlib/cCHCAttributes.ml +++ b/CodeHawk/CHC/cchlib/cCHCAttributes.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2024 Aarno Labs LLC + Copyright (c) 2024-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 diff --git a/CodeHawk/CHC/cchlib/cCHCAttributes.mli b/CodeHawk/CHC/cchlib/cCHCAttributes.mli index e763560a..2bf4207c 100644 --- a/CodeHawk/CHC/cchlib/cCHCAttributes.mli +++ b/CodeHawk/CHC/cchlib/cCHCAttributes.mli @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2024 Aarno Labs LLC + Copyright (c) 2024-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 @@ -50,7 +50,7 @@ open CCHLibTypes option is for the user to construct these summaries in xml and supply them to the analyzer as an additional set of summaries. While this may be the preferred option if the library in question is a frequently used one (e.g., - opensll), but in most cases, writing function summaries in xml is not + openssl), but in most cases, writing function summaries in xml is not attractive. Another, more convenient, option is to annotate the function signatures @@ -189,7 +189,7 @@ open CCHLibTypes (** {3 nonnull} - The [nonnull] attribute can be used to a function to indicate that one or + The [nonnull] attribute can be used for a function to indicate that one or more pointer arguments to the function must not be null. Example: @@ -214,7 +214,7 @@ open CCHLibTypes (** {3 null_terminated_string_arg} The [null_terminated_string_arg] can be used to indicate that one or more - pointer arguments must, if not null, point to null-terminated string. + pointer arguments must, if not null, point to a null-terminated string. Example: @@ -223,7 +223,7 @@ open CCHLibTypes __attribute__((__null_terminated_string_arg (2))); ]} - This attribute will generate [XNullTerminated] preconditions on the funtion + This attribute will generate [XNullTerminated] preconditions on the function for all arguments included. *) @@ -233,7 +233,7 @@ open CCHLibTypes on the program state except for the value they return. It differs from the [const] attribute in that it may read values from the program state and so successive calls to the function with the same argument may, - unlike to functions with the [const] attribute, have different return + unlike functions with the [const] attribute, have different return values. This attribute will generate the [XPreservesAllMemory] and