CHB:ARM: save typing rule applications

Author: sipma

CodeHawk/CH/xprlib/xsimplify.ml

@@ -1040,6 +1040,10 @@ and reduce_ne m e1 e2 =
      (* (a - b) != 0  ===>  a != b *)
      | (XOp (XMinus, [x; y]), SConst a) when zero_num a -> (true, XOp (XNe, [x; y]))
 
+     (* (a + b) != 0 ====> a != -b *)
+     | (XOp (XPlus, [x; y]), SConst a) when zero_num a ->
+        (true, XOp (XNe, [x; (XOp (XNeg, [y]))]))
+
      | _ -> default
 
 

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250716"
-  ~date:"2025-07-16"
+  ~version:"0.6.0_20250722"
+  ~date:"2025-07-22"
   ~licensee: None
   ~maxfilesize: None
   ()

CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml

@@ -304,8 +304,7 @@ object (self)
            save_vars faddr vard
          end );
            (* (if save then fndata#save); *)
-      H.add table fn#get_address#to_hex_string fn;
-      typeconstraints#record_type_constraints;
+      H.add table fn#get_address#to_hex_string fn
     end
 
   method write_xml (node:xml_element_int) =
@@ -325,9 +324,12 @@ object (self)
 
   method save =
     let node = xmlElement "application-results" in
+    let tcnode = xmlElement "type-constraint-store" in
     begin
       self#write_xml node;
-      save_resultdata_file node
+      save_resultdata_file node;
+      typeconstraintstore#write_xml tcnode;
+      save_typeconstraintstore tcnode
     end
 
 end

CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml

@@ -735,6 +735,9 @@ object (self:'a)
   method is_pc_register =
     match kind with ARMReg ARPC -> true | _ -> false
 
+  method is_sp_register =
+    match kind with ARMReg ARSP -> true | _ -> false
+
   method is_double_register =
     match kind with ARMDoubleReg _ -> true | _ -> false
 

CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli

@@ -202,6 +202,7 @@ class type arm_operand_int =
     method is_register: bool
     method is_shifted_register: bool
     method is_pc_register: bool
+    method is_sp_register: bool
     method is_double_register: bool
     method is_extension_register: bool
     method is_double_extension_register: bool

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

@@ -2385,6 +2385,7 @@ object (self)
              let r0_op = arm_register_op AR0 RD in
              let xr0_r = r0_op#to_expr floc in
              let xxr0_r = TR.tmap rewrite_expr xr0_r in
+             let xxr0_r = TR.tmap (rewrite_in_cc_context floc c) xxr0_r in
              let cxr0_r = TR.tbind floc#convert_xpr_to_c_expr xxr0_r in
              add_return_value tags args xr0_r xxr0_r cxr0_r
            else