Liftingarm

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/bCHFloc.ml

@@ -1259,6 +1259,10 @@ object (self)
             memref_r memoff_r
 
   method private get_variable_type (v: variable_t): btype_t traceresult =
+    let is_zero (x: xpr_t) =
+      match x with
+      | XConst (IntConst n) -> n#equal numerical_zero
+      | _ -> false in
     if self#f#env#is_initial_register_value v then
       let reg_r = self#f#env#get_initial_register_value_register v in
       TR.tbind
@@ -1348,6 +1352,43 @@ object (self)
                         let cinfo = get_compinfo_by_key ckey in
                         let finfo = get_compinfo_field cinfo fname in
                         Ok finfo.bftype
+                     | IndexOffset (v, i, memsuboff) ->
+                        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                               ^ "index offset: "
+                               ^ (memory_offset_to_string memoff)
+                               ^ " with "
+                               ^ (p2s v#toPretty)
+                               ^ ", index: "
+                               ^ (string_of_int i)
+                               ^ "; and "
+                               ^ (memory_offset_to_string memsuboff)]
+                     | ArrayIndexOffset (x, memsuboff) ->
+                        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                               ^ "array index offset: "
+                               ^ (memory_offset_to_string memoff)
+                               ^ " with "
+                               ^ (x2s x)
+                               ^ "; and "
+                               ^ (memory_offset_to_string memsuboff)]
+                     | BasePtrArrayIndexOffset (x, _) when is_zero x ->
+                        (match basevartype with
+                         | TPtr (t, _) -> Ok t
+                         | _ ->
+                            Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                                   ^ "array index offset: "
+                                   ^ (memory_offset_to_string memoff)
+                                   ^ " with basevar type: "
+                                   ^ (btype_to_string basevartype)
+                                   ^ " not yet handled"])
+                     | BasePtrArrayIndexOffset (x, memsuboff) ->
+                        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                               ^ "base-ptr array index offset: "
+                               ^ (memory_offset_to_string memoff)
+                               ^ " with "
+                               ^ (x2s x)
+                               ^ "; and "
+                               ^ (memory_offset_to_string memsuboff)]
+
                      | _ ->
                         Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
                                ^ "memoff: " ^ (memory_offset_to_string memoff)

CodeHawk/CHB/bchlib/bCHFunctionData.ml

@@ -280,6 +280,32 @@ object (self)
            __FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
            ^ "No stackvar annotation found at offset " ^ (string_of_int offset)]
 
+  method is_typing_rule_enabled (loc: string) (name: string): bool =
+    match self#get_function_annotation with
+    | None -> false
+    | Some a ->
+       List.fold_left
+         (fun acc tra ->
+           acc ||
+             (if tra.tra_action = "enable" && tra.tra_name = name then
+                (List.mem "all" tra.tra_locations)
+                || (List.mem loc tra.tra_locations)
+              else
+                false)) false a.typingrules
+
+  method is_typing_rule_disabled (loc: string) (name: string): bool =
+    match self#get_function_annotation with
+    | None -> false
+    | Some a ->
+       List.fold_left
+         (fun acc tra ->
+           acc ||
+             (if tra.tra_action = "disable" && tra.tra_name = name then
+                (List.mem "all" tra.tra_locations)
+                || (List.mem loc tra.tra_locations)
+              else
+                false)) false a.typingrules
+
   method add_inlined_block (baddr:doubleword_int) =
     inlined_blocks <- baddr :: inlined_blocks
 
@@ -592,6 +618,25 @@ let read_xml_stackvar_intro (node: xml_element_int): stackvar_intro_t traceresul
         svi_cast = svi_cast}
 
 
+let read_xml_typing_rule (node: xml_element_int): typing_rule_t traceresult =
+  let get = node#getAttribute in
+  let has = node#hasNamedAttribute in
+  if not (has "name") then
+    Error ["typingrule without name"]
+  else if not (has "locs") then
+    Error ["typingrule without location"]
+  else if not (has "action") then
+    Error ["typingrule without action"]
+  else
+    let name = get "name" in
+    let action = get "action" in
+    let locs = get "locs" in
+    let locs = String.split_on_char ',' locs in
+    Ok {tra_name = name;
+        tra_action = action;
+        tra_locations = locs}
+
+
 let read_xml_function_annotation (node: xml_element_int) =
   let get = node#getAttribute in
   let getc = node#getTaggedChild in
@@ -635,8 +680,27 @@ let read_xml_function_annotation (node: xml_element_int) =
               (rvintros#getTaggedChildren "vintro")
           else
             [] in
+        let typingrules =
+          if hasc "typing-rules" then
+            let trules = getc "typing-rules" in
+            List.fold_left
+              (fun acc n ->
+                TR.tfold
+                  ~ok:(fun tr -> tr :: acc)
+                  ~error:(fun e ->
+                    begin
+                      log_error_result __FILE__ __LINE__ e;
+                      acc
+                    end)
+                  (read_xml_typing_rule n))
+              []
+              (trules#getTaggedChildren "typingrule")
+          else
+            [] in
         fndata#set_function_annotation
-          {regvarintros = regvintros; stackvarintros = stackvintros}
+          {regvarintros = regvintros;
+           stackvarintros = stackvintros;
+          typingrules = typingrules}
       else
         log_error_result
           ~tag:"function annotation faddr not found"

CodeHawk/CHB/bchlib/bCHFunctionInterface.ml

@@ -1139,7 +1139,7 @@ let record_function_interface_type_constraints
                   ~tag:("function-interface type constraint")
                   __FILE__ __LINE__
                   [faddr ^ ": " ^ (type_constraint_to_string tyc)] in
-              store#add_constraint tyc
+              store#add_constraint faddr "exit" "INTF-freturn" tyc
            | _ -> ());
           (match fargs with
            | None ->
@@ -1160,7 +1160,7 @@ let record_function_interface_type_constraints
                                ~tag:("function-interface type constraint")
                                __FILE__ __LINE__
                                [faddr ^ ": " ^ (type_constraint_to_string tyc)] in
-                           store#add_constraint tyc
+                           store#add_constraint faddr "init" "INTF-fparam" tyc
                         | _ ->
                            chlog#add
                              "function interface type constraints"

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -1511,10 +1511,17 @@ type stackvar_intro_t = {
     svi_cast: bool
   }
 
+type typing_rule_t = {
+    tra_action: string;
+    tra_name: string;
+    tra_locations: string list
+  }
+
 
 type function_annotation_t = {
     regvarintros: regvar_intro_t list;
-    stackvarintros: stackvar_intro_t list
+    stackvarintros: stackvar_intro_t list;
+    typingrules: typing_rule_t list
   }
 
 class type function_data_int =
@@ -1567,6 +1574,8 @@ 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_typing_rule_enabled: string -> string -> bool
+    method is_typing_rule_disabled: string -> string -> bool
     method has_class_info: bool
     method has_callsites: bool
     method has_path_contexts: bool
@@ -3188,6 +3197,14 @@ type type_constraint_t =
   | TyZeroCheck of type_term_t
 
 
+type type_inference_rule_application_t = {
+    tir_faddr: string;
+    tir_loc: string;
+    tir_rule: string;
+    tir_constraint_ix: int
+  }
+
+
 class type type_constraint_dictionary_int =
   object
 
@@ -3246,17 +3263,21 @@ class type type_constraint_store_int =
 
     method reset: unit
 
-    method add_constraint: type_constraint_t -> unit
+    method add_constraint:
+             string -> string -> string -> type_constraint_t -> unit
 
-    method add_var_constraint: type_variable_t -> unit
+    method add_var_constraint:
+             string -> string -> string -> type_variable_t -> unit
 
-    method add_term_constraint: type_term_t -> unit
+    method add_term_constraint:
+             string -> string -> string -> type_term_t -> unit
 
-    method add_zerocheck_constraint: type_variable_t -> unit
+    (* method add_zerocheck_constraint: type_variable_t -> unit *)
 
-    method add_subtype_constraint: type_term_t -> type_term_t -> unit
+    method add_subtype_constraint:
+             string -> string -> string -> type_term_t -> type_term_t -> unit
 
-    method add_ground_constraint: type_term_t -> type_term_t -> unit
+    (* method add_ground_constraint: type_term_t -> type_term_t -> unit *)
 
     method get_function_type_constraints: string -> type_constraint_t list
 
@@ -3287,6 +3308,8 @@ class type type_constraint_store_int =
 
     method resolve_local_stack_lhs_types: string -> (int * btype_t option) list
 
+    method write_xml: xml_element_int -> unit
+
     method toPretty: pretty_t
 
   end

CodeHawk/CHB/bchlib/bCHPreFileIO.ml

@@ -439,6 +439,13 @@ let get_resultdata_filename () =
   Filename.concat fdir (exename ^ "_data.xml")
 
 
+let get_typeconstraintstore_filename () =
+  let exename = get_filename () in
+  let fdir = get_results_dir () in
+  let _ = create_directory fdir in
+  Filename.concat fdir (exename ^ "_tcstore.xml")
+
+
 let get_x86dictionary_filename  () =
   let exename = get_filename () in
   let fdir = get_results_dir () in
@@ -657,6 +664,18 @@ let save_resultdata_file (node:xml_element_int) =
     file_output#saveFile filename doc#toPretty
   end
 
+
+let save_typeconstraintstore (node: xml_element_int) =
+  let filename = get_typeconstraintstore_filename () in
+  let doc = xmlDocument () in
+  let root = get_bch_root "type-constraint-store" in
+  begin
+    doc#setNode root;
+    root#appendChildren [node];
+    file_output#saveFile filename doc#toPretty
+  end
+
+
 let save_cfgs (node:xml_element_int) =
   let filename = get_cfgs_filename () in
   let doc = xmlDocument () in

CodeHawk/CHB/bchlib/bCHPreFileIO.mli

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2019 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
@@ -117,7 +117,8 @@ val save_userdata_function_summary_file: string -> xml_element_int -> unit
 val save_userdata_function_summaries_file: xml_element_int -> unit
 
 val load_export_ordinal_table: string -> xml_element_int option
-val save_resultdata_file    : xml_element_int -> unit
+val save_resultdata_file: xml_element_int -> unit
+val save_typeconstraintstore: xml_element_int -> unit
 val save_cfgs: xml_element_int -> unit
 
 val save_executable_dump: xml_element_int -> unit