Merge pull request #174 from sipma/summaries

Summaries

Author: sipma

.github/workflows/dune.yaml

@@ -31,7 +31,7 @@ jobs:
     - name: Prepare tar file for upload
       run: tar -hcvf artifacts.tar CodeHawk/_build/install/default/bin/*
     - name: Upload artifacts tar file
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: artifacts-${{ matrix.ocaml-compiler }}
         path: artifacts.tar
@@ -54,7 +54,7 @@ jobs:
     - name: Delete submitted prebuilts
       run: rm -f chb/bin/binaries/linux/chx86_analyze
     - name: Download artifacts tar
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: artifacts-${{ matrix.ocaml-compiler }}
     - name: Extract artifacts
@@ -84,7 +84,7 @@ jobs:
         rm -f chc/bin/linux/parseFile
         rm -f chc/bin/linux/canalyzer
     - name: Download artifacts tar
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: artifacts-${{ matrix.ocaml-compiler }}
     - name: Extract artifacts

.github/workflows/makefiles.yaml

@@ -24,7 +24,7 @@ jobs:
     - name: Prepare tar file for upload
       run: tar -cvf artifacts.tar CodeHawk/CHB/bchcmdline/chx86_analyze CodeHawk/CHC/cchcil/parseFile CodeHawk/CHC/cchcmdline/canalyzer
     - name: Upload artifacts tar file
-      uses: actions/upload-artifact@v3
+      uses: actions/upload-artifact@v4
       with:
         name: artifacts-${{ matrix.ocaml-compiler }}
         path: artifacts.tar
@@ -45,7 +45,7 @@ jobs:
     - name: Delete submitted prebuilts
       run: rm -f chb/bin/binaries/linux/chx86_analyze
     - name: Download artifacts tar
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: artifacts-${{ matrix.ocaml-compiler }}
     - name: Extract artifacts
@@ -73,7 +73,7 @@ jobs:
         rm -f chc/bin/linux/parseFile
         rm -f chc/bin/linux/canalyzer
     - name: Download artifacts tar
-      uses: actions/download-artifact@v3
+      uses: actions/download-artifact@v4
       with:
         name: artifacts-${{ matrix.ocaml-compiler }}
     - name: Extract artifacts

CodeHawk/CH/chutil/cHLogger.ml

@@ -6,7 +6,7 @@
  
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020      Henny B. Sipma
-   Copyright (c) 2021-2024 Aarno Labs LLC
+   Copyright (c) 2021-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
@@ -226,3 +226,29 @@ let log_tfold_default
        log_tracelog_error logspec e;
        d
      end
+
+
+let log_error_result
+      ?(msg="")
+      ?(tag="")
+      (filename: string)
+      (linenumber: int)
+      (error: string list) =
+  let tag = if tag = "" then tag else tag ^ ":" in
+  let msg = if msg = "" then msg else msg ^ ": " in
+  ch_error_log#add
+    (tag ^ filename ^ ":" ^ (string_of_int linenumber))
+    (LBLOCK [STR msg; STR (String.concat "; " error)])
+
+
+let log_result
+      ?(msg="")
+      ?(tag="")
+      (filename: string)
+      (linenumber: int)
+      (error: string list) =
+  let tag = if tag = "" then tag else tag ^ ":" in
+  let msg = if msg = "" then msg else msg ^ ":" in
+  chlog#add
+    (tag ^ filename ^ ":" ^ (string_of_int linenumber))
+    (LBLOCK [STR msg; STR (String.concat "; " error)])

CodeHawk/CH/chutil/cHLogger.mli

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020-2021 Henny B. Sipma
-   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
@@ -112,3 +112,19 @@ val log_tfold:
     [e] is logged according [tls].*)
 val log_tfold_default:
   tracelogspec_t -> ('a -> 'c) -> 'c -> 'a traceresult -> 'c
+
+
+(** [log_error_result msg tag filename linenumber error] writes an entry to
+    [ch_error_log] with a tag that combines [tag], [filename], and [linenumber].
+    The entry is the concatenation of [msg] and the list of error messages
+    making up [error].*)
+val log_error_result:
+  ?msg:string -> ?tag:string -> string -> int -> string list -> unit
+
+
+(** [log_result msg tag filename linenumber error] writes an entry to
+    [chlog] with a tag that combines [tag], [filename], and [linenumber].
+    The entry is the concatenation of [msg] and the list of error messages
+    making up [error].*)
+val log_result:
+  ?msg:string -> ?tag:string -> string -> int -> string list -> unit

CodeHawk/CH/chutil/cHTraceResult.ml

@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2023-2024  Aarno Labs LLC
+   Copyright (c) 2023-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
@@ -61,6 +61,25 @@ let tmap2
   | Error e1, Error e2 -> Error (msg1 :: msg2 :: (e1 @ e2))
 
 
+let tmap3
+      ?(msg1="")
+      ?(msg2="")
+      ?(msg3="")
+      (f: 'a -> 'b -> 'c -> 'd)
+      (r1: 'a traceresult)
+      (r2: 'b traceresult)
+      (r3: 'c traceresult): 'd traceresult =
+  match r1, r2, r3 with
+  | Ok v1, Ok v2, Ok v3 -> Ok (f v1 v2 v3)
+  | Error e1, Ok _, Ok _ -> Error (msg1 :: e1)
+  | Ok _, Error e2, Ok _ -> Error (msg2 :: e2)
+  | Ok _, Ok _, Error e3 -> Error (msg3 :: e3)
+  | Error e1, Error e2, Ok _ -> Error (msg1 :: msg2 :: (e1 @ e2))
+  | Error e1, Ok _, Error e3 -> Error (msg1 :: msg3 :: (e1 @ e3))
+  | Ok _, Error e2, Error e3 -> Error (msg2 :: msg3 :: (e2 @ e3))
+  | Error e1, Error e2, Error e3 -> Error (msg1 :: msg2 :: msg3 :: (e1 @ e2 @ e3))
+
+
 let tbind ?(msg="") (f: 'a -> 'c traceresult) (r: 'a traceresult) =
   match r with
   | Ok v -> f v
@@ -86,7 +105,13 @@ let tprop (r: 'a traceresult) (msg: string): 'a traceresult =
   | Error e -> Error (msg :: e)
 
 
-let titer (f: 'a -> unit) (r: 'a traceresult) =
+let titer ~(ok:'a -> unit) ~(error: string list -> unit) (r: 'a traceresult) =
+  match r with
+  | Ok v -> ok v
+  | Error e -> error e
+
+
+let titer_default (f: 'a -> unit) (r: 'a traceresult) =
   match r with
   | Ok v -> f v
   | Error _ -> ()

CodeHawk/CH/chutil/cHTraceResult.mli

@@ -65,6 +65,20 @@ val tmap2:
   -> 'c traceresult
 
 
+(** [tmap3 f r1 r2 r3] is [Ok (f v1 v2 v3)] if [r1] is [Ok v1] and [r2] is
+    [Ok v2] and [r3] is [Ok v3]; otherwise it returns an [Error] appending
+    the messages corresponding to the error value as appropriate.*)
+val tmap3:
+  ?msg1:string
+  -> ?msg2:string
+  -> ?msg3:string
+  -> ('a -> 'b -> 'c -> 'd)
+  -> 'a traceresult
+  -> 'b traceresult
+  -> 'c traceresult
+  -> 'd traceresult
+
+
 (** [tfold ~ok ~error r] is [ok v] if [r] is [Ok v] and [error e] if [r] is
     [Error e].*)
 val tfold: ok:('a -> 'c) -> error:(string list -> 'c) -> 'a traceresult -> 'c
@@ -86,8 +100,13 @@ val tbind:
   ?msg:string -> ('a -> 'c traceresult) -> ('a traceresult) -> 'c traceresult
 
 
-(** [titer f r] is [f v] if [r] is [Ok v] and [()] otherwise.*)
-val titer: ('a -> unit) -> ('a traceresult) -> unit
+(** [titer ~ok ~error r] is [ok v] if [r] is [Ok v] and [error e] if [r] is
+    [Error e].*)
+val titer: ok:('a -> unit) -> error:(string list -> unit) -> ('a traceresult) -> unit
+
+
+(** [titer_default f r] is [f v] if [r] is [Ok v] and [()] otherwise.*)
+val titer_default: ('a -> unit) -> 'a traceresult -> unit
 
 
 (** [tfold_list ~ok init rl] folds [Ok] values left to right, starting from

CodeHawk/CHB/bchanalyze/bCHFileIO.ml

@@ -200,6 +200,19 @@ let save_global_state () =
     file_output#saveFile filename doc#toPretty
   end
 
+
+let save_global_memory_map () =
+  let filename = get_global_memory_map_filename () in
+  let doc = xmlDocument () in
+  let root = get_bch_root "global-locations" in
+  let gNode = xmlElement "global-locations" in
+  begin
+    BCHGlobalMemoryMap.global_memory_map#write_xml gNode;
+    doc#setNode root;
+    root#appendChildren [gNode];
+    file_output#saveFile filename doc#toPretty
+  end
+
 let save_system_info () =
   let filename = get_system_info_filename () in
   let doc = xmlDocument () in

CodeHawk/CHB/bchanalyze/bCHFileIO.mli

@@ -43,6 +43,7 @@ val save_functions_list: unit -> unit
 val save_arm_functions_list: unit -> unit
 
 val save_global_state: unit -> unit
+val save_global_memory_map: unit -> unit
 val save_system_info: unit -> unit
 val save_resultmetrics: xml_element_int -> unit
 val save_disassembly_status: unit -> unit

CodeHawk/CHB/bchanalyze/bCHTrace.ml

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2020 Kestrel Technology LLC
    Copyright (c) 2020      Henny Sipma
-   Copyright (c) 2021-2024 Aarno Labs LLC
+   Copyright (c) 2021-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
@@ -76,10 +76,13 @@ let se_address_is_referenced
   if floc#is_address x then
     let (memref,memoffset) = floc#decompose_address x in
     if is_constant_offset memoffset then
-      let memv =
-        finfo#env#mk_memory_variable memref (get_total_constant_offset memoffset) in
-      let memx = floc#rewrite_variable_to_external memv in
-      var_is_referenced finfo memx v
+      TR.tfold_default
+        (fun offset ->
+          let memv = finfo#env#mk_memory_variable memref offset in
+          let memx = floc#rewrite_variable_to_external memv in
+          var_is_referenced finfo memx v)
+        false
+        (get_total_constant_offset memoffset)
     else
       false
   else

CodeHawk/CHB/bchcil/bCHParseCilFile.ml

@@ -38,30 +38,25 @@ open CHLogger
 (* bchlib *)
 open BCHBCFiles
 open BCHBCTypes
-open BCHBCTypePretty
 open BCHBCTypeUtil
 open BCHCilToCBasic
-open BCHConstantDefinitions
 
 
 let update_symbolic_address_types () =
-  let globalvarnames = get_untyped_symbolic_address_names () in
-  begin
-    List.iter (fun name ->
-        if bcfiles#has_varinfo name then
-          let vinfo = bcfiles#get_varinfo name in
-          begin
-            update_symbolic_address_btype name vinfo.bvtype;
-            chlog#add
-              "symbolic address: update with vinfo"
-              (LBLOCK [STR name; STR ": "; STR (btype_to_string vinfo.bvtype)])
-          end
-        else
-          chlog#add "symbolic address: no update" (STR name)) globalvarnames;
-    chlog#add
-      "symbolic address updates"
-      (LBLOCK [STR "Names: "; STR (String.concat ", " globalvarnames)])
-  end
+  let gfunnames = bcfiles#get_gfun_names in
+  let varinfos = bcfiles#get_varinfos in
+  List.iter
+    (fun vinfo ->
+      if List.mem vinfo.bvname gfunnames then
+        ()
+      else
+        match BCHGlobalMemoryMap.update_global_location_type vinfo with
+        | Error e ->
+           ch_error_log#add
+             "update-global-location-type"
+             (LBLOCK [
+                  STR "varinfo: "; STR vinfo.bvname; STR (String.concat "; " e)])
+        | _ -> ()) varinfos
 
 
 let parse_cil_file ?(computeCFG=true) ?(removeUnused=true) (filename: string) =