From f91737eeb7632c4dab5ef39da08f23f27ebbeb61 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 29 Mar 2026 16:16:51 -0700 Subject: [PATCH 1/5] CHB:summaries:change FILE to ch_FILE type --- CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/clearerr.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/crypt.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fclose.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/feof.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/ferror.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fflush.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fgetpos.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fgets.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fileno.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fopen.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fprintf.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fputc.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fputs.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fread.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fscanf.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fseek.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fsetpos.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/ftell.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/getline.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/pclose.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/popen.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/realpath.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/rewind.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/ungetc.xml | 2 +- CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml | 2 +- 31 files changed, 31 insertions(+), 31 deletions(-) diff --git a/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml b/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml index 69e1d002..97b8734c 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/__fgetc_unlocked.xml @@ -16,7 +16,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml b/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml index eafe11d7..504f34ea 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/__fputc_unlocked.xml @@ -27,7 +27,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/clearerr.xml b/CodeHawk/CHB/bchsummaries/so_functions/clearerr.xml index 84b0514f..d55e577d 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/clearerr.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/clearerr.xml @@ -13,7 +13,7 @@ - FILE + ch_FILE
void diff --git a/CodeHawk/CHB/bchsummaries/so_functions/crypt.xml b/CodeHawk/CHB/bchsummaries/so_functions/crypt.xml index 24b821f7..09b6722d 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/crypt.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/crypt.xml @@ -31,7 +31,7 @@
- char> + char
char diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fclose.xml b/CodeHawk/CHB/bchsummaries/so_functions/fclose.xml index 49819697..35baaf51 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fclose.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fclose.xml @@ -17,7 +17,7 @@ int - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml b/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml index 844d421c..74c8a2f4 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fdopen.xml @@ -33,7 +33,7 @@ char
- FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/feof.xml b/CodeHawk/CHB/bchsummaries/so_functions/feof.xml index 7a5d3a85..39585e07 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/feof.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/feof.xml @@ -16,7 +16,7 @@ - FILE + ch_FILE diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ferror.xml b/CodeHawk/CHB/bchsummaries/so_functions/ferror.xml index dd208f3c..ffce8f9e 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/ferror.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/ferror.xml @@ -16,7 +16,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fflush.xml b/CodeHawk/CHB/bchsummaries/so_functions/fflush.xml index e580721e..b61e06bc 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fflush.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fflush.xml @@ -17,7 +17,7 @@ int - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml b/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml index f83baf3f..90515f2b 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fgetc.xml @@ -16,7 +16,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fgetpos.xml b/CodeHawk/CHB/bchsummaries/so_functions/fgetpos.xml index 510b2f61..c35159db 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fgetpos.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fgetpos.xml @@ -22,7 +22,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml b/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml index 8ba63689..dab72e3d 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fgets.xml @@ -52,7 +52,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml b/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml index 99688644..f4496dae 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fileno.xml @@ -17,7 +17,7 @@ int - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml b/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml index 7df95f74..1f1fe514 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fopen.xml @@ -16,7 +16,7 @@ - FILE + ch_FILE char diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml b/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml index b217343c..ebabb7d2 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fopen64.xml @@ -16,7 +16,7 @@ - FILE + ch_FILE char diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fprintf.xml b/CodeHawk/CHB/bchsummaries/so_functions/fprintf.xml index 088cb79d..703551ba 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fprintf.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fprintf.xml @@ -25,7 +25,7 @@ int - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml b/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml index d22dc527..01a708ec 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fputc.xml @@ -27,7 +27,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml b/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml index f28dd3f0..84bac7de 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fputs.xml @@ -33,7 +33,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fread.xml b/CodeHawk/CHB/bchsummaries/so_functions/fread.xml index c4c56721..4b8736d6 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fread.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fread.xml @@ -41,7 +41,7 @@
- FILE + ch_FILE diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fscanf.xml b/CodeHawk/CHB/bchsummaries/so_functions/fscanf.xml index fe799b87..87488ec0 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fscanf.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fscanf.xml @@ -25,7 +25,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml b/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml index c0b09158..a56d8de0 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fseek.xml @@ -25,7 +25,7 @@ int - FILE + ch_FILE diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fsetpos.xml b/CodeHawk/CHB/bchsummaries/so_functions/fsetpos.xml index 04ee20a9..2ae0d9d6 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fsetpos.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fsetpos.xml @@ -22,7 +22,7 @@ - FILE + ch_FILE diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml b/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml index ac644668..45edd6a6 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/ftell.xml @@ -17,7 +17,7 @@ long - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml b/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml index b4e945f7..e91a5032 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/fwrite.xml @@ -36,7 +36,7 @@ size_t
- FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/getline.xml b/CodeHawk/CHB/bchsummaries/so_functions/getline.xml index 6532c66e..f7fa9e0a 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/getline.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/getline.xml @@ -30,7 +30,7 @@ int
- FILE + ch_FILE
int diff --git a/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml b/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml index eb8dfa6f..a19f0da8 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/pclose.xml @@ -16,7 +16,7 @@ - FILE + ch_FILE
int diff --git a/CodeHawk/CHB/bchsummaries/so_functions/popen.xml b/CodeHawk/CHB/bchsummaries/so_functions/popen.xml index 3055a19c..f3915bd9 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/popen.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/popen.xml @@ -29,7 +29,7 @@ char
- FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml b/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml index 3ef64db5..41bc5b60 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/realpath.xml @@ -34,7 +34,7 @@
- char> + char
char diff --git a/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml b/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml index 0832e333..1e739f68 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/rewind.xml @@ -13,7 +13,7 @@ - FILE + ch_FILE
diff --git a/CodeHawk/CHB/bchsummaries/so_functions/ungetc.xml b/CodeHawk/CHB/bchsummaries/so_functions/ungetc.xml index 327c2568..36ad02d5 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/ungetc.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/ungetc.xml @@ -25,7 +25,7 @@ int
- FILE + ch_FILE diff --git a/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml b/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml index 05e622b6..ffef75bd 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/vfprintf.xml @@ -25,7 +25,7 @@ int - FILE + ch_FILE From fbcb56ce584f449030467dd1c8b04bb4a9635f87 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 29 Mar 2026 16:22:23 -0700 Subject: [PATCH 2/5] CHB:allow named types for parameter type inference --- CodeHawk/CHB/bchcil/bCHParseCilFile.ml | 5 +++ CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml | 1 + CodeHawk/CHB/bchlib/bCHBCFiles.ml | 39 ++++++++++++++++++- CodeHawk/CHB/bchlib/bCHBCTypeXml.ml | 29 +++++++++++++- CodeHawk/CHB/bchlib/bCHBCTypeXml.mli | 3 ++ CodeHawk/CHB/bchlib/bCHBCTypes.mli | 2 + CodeHawk/CHB/bchlib/bCHLibTypes.mli | 1 + CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml | 5 ++- .../CHB/bchlib/bCHTypeConstraintDictionary.ml | 2 + CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml | 12 +++++- CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +- .../bchlibarm32/bCHFnARMTypeConstraints.ml | 8 +++- 12 files changed, 102 insertions(+), 9 deletions(-) diff --git a/CodeHawk/CHB/bchcil/bCHParseCilFile.ml b/CodeHawk/CHB/bchcil/bCHParseCilFile.ml index 3987d4c0..867cb50d 100644 --- a/CodeHawk/CHB/bchcil/bCHParseCilFile.ml +++ b/CodeHawk/CHB/bchcil/bCHParseCilFile.ml @@ -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]; diff --git a/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml b/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml index 89b7c8be..567b640a 100644 --- a/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml +++ b/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml @@ -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 diff --git a/CodeHawk/CHB/bchlib/bCHBCFiles.ml b/CodeHawk/CHB/bchlib/bCHBCFiles.ml index 11122c28..1f683180 100644 --- a/CodeHawk/CHB/bchlib/bCHBCFiles.ml +++ b/CodeHawk/CHB/bchlib/bCHBCFiles.ml @@ -97,7 +97,8 @@ 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 @@ -105,6 +106,42 @@ object (self) 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 diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeXml.ml b/CodeHawk/CHB/bchlib/bCHBCTypeXml.ml index b9c134e7..28c12c41 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypeXml.ml +++ b/CodeHawk/CHB/bchlib/bCHBCTypeXml.ml @@ -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 = @@ -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, [])) @@ -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 = diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeXml.mli b/CodeHawk/CHB/bchlib/bCHBCTypeXml.mli index a8ca0496..6353b16f 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypeXml.mli +++ b/CodeHawk/CHB/bchlib/bCHBCTypeXml.mli @@ -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 diff --git a/CodeHawk/CHB/bchlib/bCHBCTypes.mli b/CodeHawk/CHB/bchlib/bCHBCTypes.mli index 4072e79a..4906916a 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHBCTypes.mli @@ -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 diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index cb6f6670..a53d6c3b 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -3296,6 +3296,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 *) diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index b72bf065..92566107 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -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 @@ -611,11 +611,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 diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml index a95030b0..b754b3a7 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml @@ -215,6 +215,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 @@ -236,6 +237,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 diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml index 940d87da..cf2c1388 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml @@ -223,6 +223,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" @@ -339,6 +340,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) @@ -477,7 +481,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 @@ -575,6 +579,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 @@ -587,6 +593,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 @@ -665,6 +674,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 diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 11121daa..74ce3ea1 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_20260324" - ~date:"2026-03-24" + ~version:"0.6.0_20260329" + ~date:"2026-03-29" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index 6d90b833..96af612b 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -313,7 +313,13 @@ object (self) end else log_type_constraint_rule_disabled __LINE__ rule tc - | _ -> ()) + | _ -> + log_diagnostics_result + ~tag:"propagate_arg_to_param:no constraint" + ~msg:(p2s floc#l#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x); + "btype: " ^ (btype_to_string argtype)]) ~error:(fun e -> log_diagnostics_result ~tag:mnem From 6a94a7042fa010770efcbb9ae28da3a377d221c6 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 29 Mar 2026 16:50:08 -0700 Subject: [PATCH 3/5] CHB: add deallocate to argument mode --- CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml | 14 ++++++++++++++ CodeHawk/CHB/bchlib/bCHLibTypes.mli | 1 + CodeHawk/CHB/bchlib/bCHSideeffect.ml | 1 + CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml | 3 ++- CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml | 4 +++- CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml | 5 +++++ CodeHawk/CHB/bchsummaries/so_functions/free.xml | 11 ++++++++++- 7 files changed, 36 insertions(+), 3 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml index 33661fce..25bb060f 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml @@ -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 diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index a53d6c3b..f083f293 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -3244,6 +3244,7 @@ type type_arg_mode_t = | ArgDerefReadWrite of int option | ArgDerefRead of int option | ArgDerefWrite of int option + | ArgDeallocate | ArgFunctionPointer | ArgScalarValue diff --git a/CodeHawk/CHB/bchlib/bCHSideeffect.ml b/CodeHawk/CHB/bchlib/bCHSideeffect.ml index 7f5010e1..eff38858 100644 --- a/CodeHawk/CHB/bchlib/bCHSideeffect.ml +++ b/CodeHawk/CHB/bchlib/bCHSideeffect.ml @@ -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)) diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index 92566107..ca141550 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -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 diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml index b754b3a7..338c27fb 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml @@ -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 @@ -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 ()) diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml index cf2c1388..55246ec1 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml @@ -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 @@ -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" @@ -468,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 diff --git a/CodeHawk/CHB/bchsummaries/so_functions/free.xml b/CodeHawk/CHB/bchsummaries/so_functions/free.xml index d2662a77..392eb255 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/free.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/free.xml @@ -27,7 +27,16 @@
- + + + + + + ptr + + + +
Copyright 2012-2016, Kestrel Technology LLC, Palo Alto, CA 94304 From 8eafcb06f545b4216b6d400cc75cd3a025902e85 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 29 Mar 2026 17:04:12 -0700 Subject: [PATCH 4/5] CHB:apply integer promotion to parameter and return types --- CodeHawk/CHB/bchlib/bCHSideeffect.ml | 2 +- CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml | 16 +++++++++++++--- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHSideeffect.ml b/CodeHawk/CHB/bchlib/bCHSideeffect.ml index eff38858..3e72aebb 100644 --- a/CodeHawk/CHB/bchlib/bCHSideeffect.ml +++ b/CodeHawk/CHB/bchlib/bCHSideeffect.ml @@ -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 diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml index 02da1b5e..06ec304b 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml @@ -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 @@ -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 @@ -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 _ = From 636a625b024ef9e0b8b105db7bbad618c343eb0e Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 29 Mar 2026 22:07:36 -0700 Subject: [PATCH 5/5] CHB:ARM: only enable POP-rdef-return when constructing signatures --- .../bchlibarm32/bCHFnARMTypeConstraints.ml | 152 ++++++++---------- 1 file changed, 68 insertions(+), 84 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index 96af612b..ca68abb5 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -336,6 +336,70 @@ object (self) "call: " ^ (p2s floc#get_call_target#toPretty)]; end in + let propagate_returnvar_to_function_return () = + let reg = register_of_arm_register AR0 in + let rvar = mk_function_typevar faddr in + let rvar = add_return_capability rvar in + let r0var = floc#env#mk_arm_register_variable AR0 in + let r0defs = get_variable_rdefs r0var in + let r0defs = + List.filter (fun d -> not (d#getBaseName = "init")) r0defs in + let rule = "POP-rdef-return" in + List.iter (fun r0def -> + let rettypeterm = mk_vty_term rvar in + let r0addr = r0def#getBaseName in + let ifloc = + get_i_floc floc (TR.tget_ok (string_to_doubleword r0addr)) in + let r0typevar = mk_reglhs_typevar reg faddr r0addr in + let r0var = floc#f#env#mk_register_variable reg in + let r0xvar = rewrite_floc_expr ifloc (XVar r0var) in + match r0xvar with + | XVar returnvar when floc#f#env#is_return_value returnvar -> + let callsite_r = floc#f#env#get_call_site returnvar in + TR.tfold_default + (fun callsite -> + if floc#f#has_call_target callsite then + let calltarget = floc#f#get_call_target callsite in + let returntype = calltarget#get_returntype in + let opttc = mk_btype_constraint rvar returntype in + let rule = "POP-rdef-inv" in + match opttc with + | Some tc -> + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc + end + else + log_type_constraint_rule_disabled __LINE__ rule tc + | _ -> + begin + log_no_type_constraint __LINE__ rule returntype; + () + end) + () + callsite_r + | _ -> + let r0typeterm = mk_vty_term r0typevar in + begin + (if fndata#is_typing_rule_enabled ~rdef:(Some r0addr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule r0typeterm rettypeterm; + store#add_subtype_constraint + faddr iaddr rule r0typeterm rettypeterm + end + else + log_subtype_rule_disabled __LINE__ rule r0typeterm rettypeterm); + (log_diagnostics_result + ~tag:"Pop" + ~msg:faddr + __FILE__ __LINE__ + ["r0addr: " ^ r0addr; + "r0xvar: " ^ (x2s r0xvar)]) + end + + ) r0defs in + let getopt_stackaddress_r (x_r: xpr_t traceresult): int option = TR.tfold_default getopt_stackaddress None x_r in @@ -1477,7 +1541,8 @@ object (self) let r0typeterm = mk_vty_term r0typevar in let rvartypeterm = mk_vty_term rvar in let lhstypeterm = mk_vty_term typevar in - if fndata#is_typing_rule_enabled ~rdef:(Some r0addr) iaddr rule then + if fndata#is_typing_rule_enabled + ~rdef:(Some r0addr) iaddr rule then begin log_subtype_constraint __LINE__ rule r0typeterm lhstypeterm; log_subtype_constraint __LINE__ rule rvartypeterm lhstypeterm; @@ -1490,89 +1555,8 @@ object (self) log_subtype_rule_disabled __LINE__ rule r0typeterm lhstypeterm ) r0defs); - (let rvar = mk_function_typevar faddr in - let rvar = add_return_capability rvar in - let r0var = floc#env#mk_arm_register_variable AR0 in - let r0defs = get_variable_rdefs r0var in - let r0defs = - List.filter (fun d -> not (d#getBaseName = "init")) r0defs in - let rule = "POP-rdef-return" in - List.iter (fun r0def -> - let rettypeterm = mk_vty_term rvar in - let r0addr = r0def#getBaseName in - let ifloc = - get_i_floc floc (TR.tget_ok (string_to_doubleword r0addr)) in - let r0typevar = mk_reglhs_typevar reg faddr r0addr in - let r0var = floc#f#env#mk_register_variable reg in - let r0xvar = rewrite_floc_expr ifloc (XVar r0var) in - match r0xvar with - | XVar returnvar when floc#f#env#is_return_value returnvar -> - let callsite_r = floc#f#env#get_call_site returnvar in - TR.tfold_default - (fun callsite -> - if floc#f#has_call_target callsite then - let calltarget = floc#f#get_call_target callsite in - let returntype = calltarget#get_returntype in - let opttc = mk_btype_constraint rvar returntype in - let rule = "POP-rdef-inv" in - match opttc with - | Some tc -> - if fndata#is_typing_rule_enabled iaddr rule then - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end - else - log_type_constraint_rule_disabled __LINE__ rule tc - | _ -> - begin - log_no_type_constraint __LINE__ rule returntype; - () - end) - () - callsite_r - (* - | XVar param when floc#f#env#is_initial_register_value param -> - let paramreg_r = floc#f#env#get_initial_register_value_register param in - let pvar = mk_function_typevar faddr in - TR.tfold - ~ok:(fun paramreg -> - let pvar = add_freg_param_capability paramreg pvar in - let ptypeterm = mk_vty_term pvar in - let rtypeterm = mk_vty_term rvar in - begin - log_subtype_constraint __LINE__ rule ptypeterm rtypeterm; - store#add_subtype_constraint - faddr iaddr rule ptypeterm rtypeterm - end) - ~error:(fun e -> - log_diagnostics_result - ~tag:"Pop" - ~msg:faddr - __FILE__ __LINE__ - [String.concat "; " e]) - paramreg_r - *) - | _ -> - let r0typeterm = mk_vty_term r0typevar in - begin - (if fndata#is_typing_rule_enabled ~rdef:(Some r0addr) iaddr rule then - begin - log_subtype_constraint __LINE__ rule r0typeterm rettypeterm; - store#add_subtype_constraint - faddr iaddr rule r0typeterm rettypeterm - end - else - log_subtype_rule_disabled __LINE__ rule r0typeterm rettypeterm); - (log_diagnostics_result - ~tag:"Pop" - ~msg:faddr - __FILE__ __LINE__ - ["r0addr: " ^ r0addr; - "r0xvar: " ^ (x2s r0xvar)]) - end - - ) r0defs) + (if self#construct_signature then + propagate_returnvar_to_function_return ()); end);