CHB: incorporate loop counters in result rewriting

Author: sipma

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -1609,6 +1609,32 @@ object (self)
       TR.tfold_default BCHBCTypeUtil.is_pointer false (self#get_xpr_type y) in
     let default () = self#convert_xpr_offsets ~xtype ~size x in
     match x with
+    | XOp (XPlus, [y; XOp (XMult, [XConst (IntConst n); XVar v])]) ->
+       let _ =
+         log_diagnostics_result
+           ~msg:(p2s self#l#toPretty)
+           ~tag:"xpr_to_cxpr:scaled expr"
+           __FILE__ __LINE__
+           ["y: " ^ (x2s y);
+            "var: " ^ (p2s v#toPretty);
+            "n: " ^ n#toString] in
+       let gloc_o = memmap#xpr_containing_location x in
+       (match gloc_o with
+        | Some gloc ->
+           let memoff_o = TR.to_option (gloc#address_memory_offset self#l x) in
+           (match memoff_o with
+            | Some memoff ->
+               let _ =
+                 log_diagnostics_result
+                   ~msg:(p2s self#l#toPretty)
+                   ~tag:"xpr_to_cxpr:scaled gloc expr"
+                   __FILE__ __LINE__
+                   [(x2s x); gloc#name; memory_offset_to_string memoff] in
+               Ok (XOp ((Xf "addressofvar"),
+                        [XVar (self#f#env#mk_gloc_variable gloc memoff)]))
+           | _ -> default ())
+        | _ -> default ())
+
     | XOp (XPlus, [y; XConst (IntConst n)]) when is_pointer y && arithm ->
        let derefty = BCHBCTypeUtil.ptr_deref (TR.tget_ok (self#get_xpr_type y)) in
        let _ =
@@ -2374,8 +2400,20 @@ object (self)
          match rhs with
          | XConst (IntConst n) when n#gt CHNumerical.numerical_zero ->
             let dw = numerical_mod_to_doubleword n in
-            if memmap#has_location dw then
-              TR.tvalue (self#f#env#mk_global_variable_address dw) ~default:rhs
+            (* do not rewrite to global addresses in the presence of loop counter
+               equalities, because the presence of symbolic constants derails the
+               generation of loop invariants. *)
+            if (memmap#has_location dw)
+               && (not (self#inv#has_loop_counter_equality)) then
+              let newrhs =
+                TR.tvalue (self#f#env#mk_global_variable_address dw) ~default:rhs in
+              let _ =
+                ch_diagnostics_log#add
+                  "rewrite constant to global address"
+                  (LBLOCK [
+                       self#l#toPretty; STR ": ";
+                       dw#toPretty; STR " ==> "; (x2p newrhs)]) in
+              newrhs
             else
               rhs
          | _ -> rhs in
@@ -2426,6 +2464,7 @@ object (self)
          let reqC = self#env#request_num_constant in
          let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in
          let cmds = rhscmds @ [ASSIGN_NUM (lhs, rhs_c)] in
+
          let fndata = self#f#get_function_data in
          match fndata#get_regvar_intro self#ia with
          | Some rvi when rvi.rvi_cast && Option.is_some rvi.rvi_vartype ->
@@ -3216,7 +3255,16 @@ object (self)
      let bridgeVars = self#env#get_bridge_values_at self#cia in
      let abstractglobals =
        let globals =
-         List.filter self#env#is_global_variable self#env#get_variables in
+         List.filter self#f#env#is_mutable_global_variable self#env#get_variables in
+       let _ =
+         ch_diagnostics_log#add
+           "call: abstract globals"
+           (LBLOCK [
+                self#l#toPretty; STR ": ";
+                pretty_print_list
+                  globals
+                  (fun v -> STR (self#f#env#variable_name_to_string v))
+                  "[" ", " "]"]) in
        [ABSTRACT_VARS globals] in
      let sideeffect_assigns =
        self#get_sideeffect_assigns termev self#get_call_target#get_semantics in

CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml

@@ -107,6 +107,8 @@ object (self)
     | Ok t -> is_scalar t
     | _ -> false
 
+  method is_loopcounter: bool = sslot.sslot_loopcounter
+
   method size: int option = sslot.sslot_size
 
   method desc = sslot.sslot_desc
@@ -365,6 +367,7 @@ object (self)
                   sslot_name = svintro.svi_name;
                   sslot_btype = ty;
                   sslot_spill = None;
+                  sslot_loopcounter = svintro.svi_loopcounter;
                   sslot_desc = Some ("svintro");
                   sslot_size = size} in
               let stackslot = new stackslot_t sslot in
@@ -449,6 +452,7 @@ object (self)
              sslot_btype = btype;
              sslot_spill = spill;
              sslot_size = size;
+             sslot_loopcounter = false;
              sslot_desc = desc
            } in
          let sslot = new stackslot_t ssrec in
@@ -495,6 +499,7 @@ object (self)
                sslot_btype = t_unknown;
                sslot_spill = Some reg;
                sslot_size = Some 4;
+               sslot_loopcounter = false;
                sslot_desc = Some "register spill"
              } in
            let sslot = new stackslot_t ssrec in
@@ -534,6 +539,7 @@ object (self)
                sslot_btype = t_unknown;
                sslot_spill = Some reg;
                sslot_size = Some 4;
+               sslot_loopcounter = false;
                sslot_desc = Some "register_spill"
              } in
            let sslot = new stackslot_t ssrec in
@@ -571,7 +577,20 @@ object (self)
            (iaddr:ctxt_iaddress_t) =
     let ty = match typ with Some t -> t | _ -> t_unknown in
     let blread = StackBlockRead (offset, size, ty) in
-    self#add_access offset iaddr blread
+    let ssrec = {
+        sslot_name = "blockread";
+        sslot_offset = offset;
+        sslot_btype = ty;
+        sslot_size = size;
+        sslot_spill = None;
+        sslot_loopcounter = false;
+        sslot_desc = None
+      } in
+    let sslot = new stackslot_t ssrec in
+    begin
+      self#add_access offset iaddr blread;
+      H.add stackslots offset sslot
+    end
 
   method add_block_write
            ~(offset:int)

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -1511,7 +1511,8 @@ type stackvar_intro_t = {
     svi_offset: int;
     svi_name: string;
     svi_vartype: btype_t option;
-    svi_cast: bool
+    svi_cast: bool;
+    svi_loopcounter: bool
   }
 
 type typing_rule_t = {
@@ -1531,7 +1532,8 @@ type function_annotation_t = {
     regvarintros: regvar_intro_t list;
     stackvarintros: stackvar_intro_t list;
     typingrules: typing_rule_t list;
-    reachingdefspecs: reachingdef_spec_t list
+    reachingdefspecs: reachingdef_spec_t list;
+    constglobalvars: string list
   }
 
 class type function_data_int =
@@ -1592,6 +1594,7 @@ class type function_data_int =
     method has_regvar_type_cast: doubleword_int -> bool
     method has_stackvar_type_annotation: int -> bool
     method has_stackvar_type_cast: int -> bool
+    method is_const_global_variable: string -> bool
     method filter_deflocs: string -> variable_t -> symbol_t list -> symbol_t list
     method is_typing_rule_enabled: ?rdef:string option -> string -> string -> bool
     method has_class_info: bool
@@ -1858,11 +1861,13 @@ object ('a)
   method get_fact: invariant_fact_t
   method get_variables: variable_t list
   method get_variable_equality_variables: variable_t list
+  method get_var_loopcounter_expr: variable_t -> xpr_t option
   method is_constant: bool
   method is_interval: bool
   method is_base_offset_value: bool
   method is_symbolic_expr: bool
   method is_linear_equality: bool
+  method is_loopcounter_equality: bool
   method is_variable_equality: bool
   method is_smaller: 'a -> bool
   method write_xml: xml_element_int -> unit
@@ -1893,7 +1898,7 @@ object
   method get_known_initial_values: variable_t list
   method get_init_disequalities: variable_t list (* initial values *)
   method get_init_equalities: variable_t list (* initial values *)
-  method rewrite_expr: xpr_t ->  xpr_t
+  method rewrite_expr: ?loopcounter:bool -> xpr_t ->  xpr_t
 
   (* predicates *)
   method is_unreachable: bool
@@ -1907,6 +1912,7 @@ object
            variable_t -> ctxt_iaddress_t -> ctxt_iaddress_t -> bool
   method var_has_initial_value: variable_t -> bool
   method var_has_symbolic_expr: variable_t -> bool
+  method has_loop_counter_equality: bool
 
   (* xml *)
   method write_xml: xml_element_int -> unit
@@ -3780,6 +3786,10 @@ class type vardictionary_int =
     method xd: xprdictionary_int
     method faddr: doubleword_int
     method reset: unit
+
+    method set_av_attributes: int -> string list -> unit
+    method get_av_attributes: int -> string list
+
     method get_indexed_variables: (int * assembly_variable_denotation_t) list
     method get_indexed_bases: (int * memory_base_t) list
 
@@ -3840,6 +3850,9 @@ object
   (** Returns the memory reference manager for this function.*)
   method memrefmgr: memory_reference_manager_int
 
+  method set_av_attributes: int -> string list -> unit
+  method get_av_attributes: int -> string list
+
   (** {1 Creating variables}*)
 
   (** {2 Registers and flags}*)
@@ -4580,6 +4593,7 @@ end
     sslot_btype: btype_t;
     sslot_size: int option;
     sslot_spill: register_t option;
+    sslot_loopcounter: bool;
     sslot_desc: string option
   }
 
@@ -4612,6 +4626,7 @@ class type stackslot_int =
     method is_struct: bool
     method is_array: bool
     method is_spill: bool
+    method is_loopcounter: bool
 
     method write_xml: xml_element_int -> unit
   end
@@ -5018,6 +5033,15 @@ class type function_environment_int =
         or if [var] is the initial value of a global variable. *)
     method is_global_variable: variable_t -> bool
 
+    (** [is_mutable_global_variable var] returns [true] if [var] is a global
+        variable, but not an initial memory value and not a const global variable
+        (as annotated in the function annotations).
+
+        Note: non-mutability is asserted only in the context of a given function
+        (as derived from the function annotations).
+     *)
+    method is_mutable_global_variable: variable_t -> bool
+
     (** Returns true if [var] is a global variable with a constant offset
         (i.e., a numerical value). *)
     method has_global_variable_address: variable_t -> bool

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20251012"
-  ~date:"2025-10-12"
+  ~version:"0.6.0_20251021"
+  ~date:"2025-10-21"
   ~licensee: None
   ~maxfilesize: None
   ()