Codepcrefinement

CodeHawk/CH/xprlib/xsimplify.ml

@@ -1143,6 +1143,9 @@ and reduce_or m e1 e2 =
 	  XOp (XSubset, [ _s ; _t ]))
 	    when (is_zero y) ->
 	  (true, XOp (XLe, [ x ; z]))
+       | (XOp (XNe, [x1; y1]), XOp (XEq, [x2; y2]))
+            when syntactically_equal x1 x2 && syntactically_equal y1 y2 ->
+          (true, true_constant_expr)
        | _ ->
 	  default
 
@@ -1195,7 +1198,17 @@ and reduce_and m e1 e2 =
   else if syntactically_equal e1 e2 then
     (true, e1)
   else
-    default
+    match (e1, e2) with
+
+    (* (x == y) and (x != y) *)
+    | (XOp (XEq, [x1; y1]), XOp (XNe, [x2; y2]))
+         when syntactically_equal x1 x2 && syntactically_equal y1 y2 ->
+       (true, false_constant_expr)
+    | (XOp (XNe, [x1; y1]), XOp (XEq, [x2; y2]))
+         when syntactically_equal x1 x2 && syntactically_equal y1 y2 ->
+       (true, false_constant_expr)
+    | _ ->
+       default
 
 
 and reduce_shiftleft (m: bool) (e1: xpr_t) (e2: xpr_t): bool * xpr_t =

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -2429,20 +2429,27 @@ object (self)
       TR.tbind
         ~msg:(eloc __LINE__)
         (fun callsite ->
-          let loc = ctxt_string_to_location self#fa callsite in
-          let fndata = functions_data#get_function self#fa in
-          if fndata#has_regvar_type_annotation loc#i then
-            fndata#get_regvar_type_annotation loc#i
-          else
-            let ctinfo = self#f#get_call_target callsite in
-            let rty = ctinfo#get_returntype in
-            if is_unknown_type rty then
+          TR.tfold
+            ~ok:(fun loc ->
+              let fndata = functions_data#get_function self#fa in
+              if fndata#has_regvar_type_annotation loc#i then
+                fndata#get_regvar_type_annotation loc#i
+              else
+                let ctinfo = self#f#get_call_target callsite in
+                let rty = ctinfo#get_returntype in
+                if is_unknown_type rty then
+                  Error [(elocm __LINE__);
+                         (p2s self#l#toPretty);
+                         "return type of function " ^ ctinfo#get_name
+                         ^ " not known"]
+                else
+                  Ok rty)
+            ~error:(fun e ->
               Error [(elocm __LINE__);
                      (p2s self#l#toPretty);
-                     "return type of function " ^ ctinfo#get_name
-                     ^ " not known"]
-            else
-              Ok rty)
+                     String.concat "; " e;
+                     "location of return type of function invalid"])
+            (ctxt_string_to_location self#fa callsite))
         (self#f#env#get_call_site v)
 
     else if self#f#env#is_register_variable v then

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -1670,6 +1670,7 @@ object (self)
 
   val cc_user_to_setter = H.create 3                             (* cc-users *)
   val test_expressions = H.create 3                      (* test-expressions *)
+  val fragment_membership = H.create 3
   val test_variables = H.create 3                          (* test-variables *)
 
   (* val cvariable_types = H.create 3 *)     (* types of constant-value variables *)
@@ -2125,6 +2126,23 @@ object (self)
     let _ = H.iter (fun ix v -> result := (ix,v) :: !result) test_expressions in
     !result
 
+  method set_fragment_membership
+           (iaddr: ctxt_iaddress_t) (fm: fragment_membership_t) =
+    H.replace fragment_membership iaddr fm
+
+  method get_fragment_membership
+           (iaddr: ctxt_iaddress_t): fragment_membership_t =
+    if H.mem fragment_membership iaddr then
+      H.find fragment_membership iaddr
+    else
+      raise
+        (BCH_failure
+           (LBLOCK [STR "function_info#get_fragment_membership: ";
+                    STR iaddr]))
+
+  method has_fragment_membership (iaddr: ctxt_iaddress_t) =
+    H.mem fragment_membership iaddr
+
   method set_test_variables
            (test_iaddr: ctxt_iaddress_t)
            (vars: (variable_t * variable_t) list) =
@@ -2484,6 +2502,58 @@ object (self)
       constant_table#set v (mkNumericalFromString (n#getAttribute "value")))
       (node#getTaggedChildren "var")
 
+  method private write_xml_fragment_memberships (node: xml_element_int) =
+    let l = ref []  in
+    let _ = H.iter (fun k e -> l := (k, e) :: !l) fragment_membership in
+    let l = List.sort (fun (k1, _) (k2, _) -> Stdlib.compare k1 k2) !l in
+    begin
+      node#appendChildren
+        (List.map (fun (k, fm) ->
+             let eNode = xmlElement "fmem" in
+             begin
+               eNode#setAttribute "opener" fm.fmem_openerloc#ci;
+               eNode#setAttribute "iaddr" k;
+               eNode#setAttribute
+                 "pol" (match fm.fmem_bucket with
+                        | FragThen -> "then" | FragElse -> "else");
+               eNode
+             end) l)
+    end
+
+  method private read_xml_fragment_memberships (node: xml_element_int) =
+    let getcc = node#getTaggedChildren in
+    List.iter (fun eNode ->
+        let get = eNode#getAttribute in
+        let iaddr = get "iaddr" in
+        let faddr = self#get_address in
+        TR.tfold
+          ~ok:(fun opener ->
+            let polarity =
+              match (get "pol") with
+              | "then" -> FragThen
+              | "else" -> FragElse
+              | s ->
+                 raise
+                   (BCH_failure
+                      (LBLOCK [STR "read_xml_fragment_memberships: ";
+                               self#get_address#toPretty;
+                               STR ": ";
+                               STR s])) in
+            H.add fragment_membership iaddr
+              {fmem_openerloc = opener; fmem_bucket = polarity})
+          ~error:(fun e ->
+            begin
+              log_error_result
+                ~tag:"read_xml_fragment_memberships"
+                ~msg:faddr#to_hex_string
+                __FILE__ __LINE__ e;
+              raise
+                (BCH_failure
+                   (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)]))
+            end)
+          (BCHLocation.ctxt_string_to_location faddr (get "opener")))
+      (getcc "fmem")
+
   method private write_xml_test_expressions (node:xml_element_int) =
     let l = ref [] in
     let _ = H.iter (fun k e -> l := (k,e) :: !l) test_expressions in
@@ -2594,6 +2664,7 @@ object (self)
     let cNode = xmlElement "constants" in
     let tvNode = xmlElement "test-variables" in
     let teNode = xmlElement "test-expressions" in
+    let fmNode = xmlElement "fragment-memberships" in
     let jtNode = xmlElement "jump-targets" in
     let ctNode = xmlElement "call-targets" in
     let fsNode = xmlElement "format-strings" in
@@ -2608,6 +2679,7 @@ object (self)
       self#write_xml_constants cNode;
       self#write_xml_cc_users ccNode;
       self#write_xml_test_expressions teNode;
+      self#write_xml_fragment_memberships fmNode;
       self#write_xml_test_variables tvNode;
       (* self#write_xml_jump_targets jtNode ; *)
       self#write_xml_call_targets ctNode;
@@ -2624,6 +2696,7 @@ object (self)
           ccNode;
           tvNode;
           teNode;
+          fmNode;
           cNode;
 	  ctNode;
           fsNode;
@@ -2649,6 +2722,10 @@ object (self)
 	    self#read_xml_test_variables (getc "test-variables"));
 	(if hasc "test-expressions" then
 	   self#read_xml_test_expressions (getc "test-expressions"));
+        (*
+        (if hasc "fragment-memberships" then
+           self#read_xml_fragment_memberships (getc "fragment-memberships"));
+         *)
         (if hasc "format-strings" then
            self#read_xml_format_strings (getc "format-strings"));
 	(if hasc "base-pointers" then

CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml

@@ -139,7 +139,17 @@ let buffer_writer_callsite
                if defcia = "init" then
                  None
                else if finfo#has_call_target defcia then
-                 Some (BCHLocation.ctxt_string_to_location finfo#a defcia)
+                 TR.tfold
+                   ~ok:(fun loc -> Some loc)
+                   ~error:(fun e ->
+                     begin
+                       log_error_result
+                         ~tag:"buffer_writer_callsite"
+                         ~msg:(p2s loc#toPretty)
+                         __FILE__ __LINE__ e;
+                       None
+                     end)
+                   (BCHLocation.ctxt_string_to_location finfo#a defcia)
                else
                  None)
              vinv#get_reaching_defs)
@@ -199,7 +209,17 @@ let external_buffer_writer_callsite
             if defcia = "init" then
               None
             else if finfo#has_call_target defcia then
-              Some (BCHLocation.ctxt_string_to_location finfo#a defcia)
+              TR.tfold
+                ~ok:(fun loc -> Some loc)
+                ~error:(fun e ->
+                  begin
+                    log_error_result
+                      ~tag:"external_buffer_writer_callsite"
+                      ~msg:(p2s loc#toPretty)
+                      __FILE__ __LINE__ e;
+                    None
+                  end)
+                (BCHLocation.ctxt_string_to_location finfo#a defcia)
             else
               None)
           vinv#get_reaching_defs)
@@ -1555,33 +1575,37 @@ let impose_trusted_os_cmd_string_pc
   let* memvar = finfo#env#mk_basevar_memory_variable paramvar NoOffset in
   let errors =
     List.fold_left (fun errors rcia ->
-        let loc = BCHLocation.ctxt_string_to_location finfo#get_address rcia in
-        match external_buffer_writer_callsite finfo loc memvar with
-        | Some defloc ->
-           let deffloc = BCHFloc.get_finfo_floc finfo defloc in
-           if call_writes_to_buffer deffloc (XVar paramvar) then
-             let xpo = XPOTrustedOsCmdString (XVar paramvar) in
-             begin
-               finfo#proofobligations#add_proofobligation defloc#ci xpo Open;
-               (log_diagnostics_result
-                  ~tag:"impose_trusted_os_cmd_string_pc"
-                  ~msg:(p2s defloc#toPretty)
-                  __FILE__ __LINE__
-                  ["returnloc: " ^ rcia;
-                   "xpo: " ^ (p2s (xpo_predicate_to_pretty xpo))]);
-               errors
-             end
-           else
-             [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc";
-              "no buffer write";
-              "returnloc: " ^ rcia;
-              "deffloc: " ^ (p2s deffloc#l#toPretty);
-              "memvar: " ^ (p2s memvar#toPretty)] @ errors
-        | _ ->
-           [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc";
-            "no defloc";
-            "returnloc: " ^ rcia;
-            "memvar: " ^ (p2s memvar#toPretty)] @ errors)
+        TR.tfold
+          ~ok:(fun loc ->
+            match external_buffer_writer_callsite finfo loc memvar with
+            | Some defloc ->
+               let deffloc = BCHFloc.get_finfo_floc finfo defloc in
+               if call_writes_to_buffer deffloc (XVar paramvar) then
+                 let xpo = XPOTrustedOsCmdString (XVar paramvar) in
+                 begin
+                   finfo#proofobligations#add_proofobligation defloc#ci xpo Open;
+                   (log_diagnostics_result
+                      ~tag:"impose_trusted_os_cmd_string_pc"
+                      ~msg:(p2s defloc#toPretty)
+                      __FILE__ __LINE__
+                      ["returnloc: " ^ rcia;
+                       "xpo: " ^ (p2s (xpo_predicate_to_pretty xpo))]);
+                   errors
+                 end
+               else
+                 [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc";
+                  "no buffer write";
+                  "returnloc: " ^ rcia;
+                  "deffloc: " ^ (p2s deffloc#l#toPretty);
+                  "memvar: " ^ (p2s memvar#toPretty)] @ errors
+            | _ ->
+               [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc";
+                "no defloc";
+                "returnloc: " ^ rcia;
+                "memvar: " ^ (p2s memvar#toPretty)] @ errors)
+          ~error:(fun e ->
+            [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc"] @ e @ errors)
+          (BCHLocation.ctxt_string_to_location finfo#get_address rcia))
       [] returnlocs in
   match errors with
   | [] -> Ok ()

CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml

@@ -310,6 +310,20 @@ object (self)
              && Option.is_none tgtsize
              && Option.is_none tgtbtype ->
          Ok NoOffset
+      | XConst (IntConst n) when
+             n#equal CHNumerical.numerical_zero
+             && Option.is_some tgtbtype
+             && is_struct_type (Option.get tgtbtype)
+             && is_struct_type btype ->
+         let tgttype = Option.get tgtbtype in
+         let cinfo1 = get_struct_type_compinfo tgttype in
+         let cinfo2 = get_struct_type_compinfo btype in
+         if cinfo1.bckey = cinfo2.bckey then
+           Ok NoOffset
+         else
+           Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                  ^ "cinfo1: " ^ cinfo1.bcname
+                  ^ "; cinfo2: " ^ cinfo2.bcname]
       | XConst (IntConst _) ->
          if is_struct_type btype then
            let compinfo = get_struct_type_compinfo btype in

CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml

@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2024-2025  Aarno Labs LLC
+   Copyright (c) 2024-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
@@ -793,14 +793,24 @@ object (self)
            (btype: btype_t) =
     match self#xpr_containing_location gxpr with
     | Some gloc ->
-       let loc = BCHLocation.ctxt_string_to_location faddr iaddr in
-       let memoff = TR.to_option (gloc#address_memory_offset loc gxpr) in
-       let garg =
-         GAddressArgument (gloc#address, iaddr, argindex, gxpr, btype, memoff) in
-       begin
-         self#add_global_ref faddr garg;
-         Some gloc
-       end
+       TR.tfold
+         ~ok:(fun loc ->
+           let memoff = TR.to_option (gloc#address_memory_offset loc gxpr) in
+           let garg =
+             GAddressArgument (gloc#address, iaddr, argindex, gxpr, btype, memoff) in
+           begin
+             self#add_global_ref faddr garg;
+             Some gloc
+           end)
+         ~error:(fun e ->
+           begin
+             log_error_result
+               ~tag:"add_gaddr_argument"
+               ~msg:iaddr
+               __FILE__ __LINE__ e;
+             None
+           end)
+         (BCHLocation.ctxt_string_to_location faddr iaddr)
     | _ ->
        (match gxpr with
         | XConst (IntConst n) ->

CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml

@@ -403,7 +403,7 @@ object (self)
     let getdw (s: string) = TR.tget_ok (string_to_doubleword s) in
     let makeloc (faddr: string) (ci: string) =
       let dw = TR.tget_ok (string_to_doubleword faddr) in
-      ctxt_string_to_location dw ci in
+      TR.tget_ok (ctxt_string_to_location dw ci) in
     let t = t name tags in
     let a = a name args in
     match (t 0) with