CHB:TYP: infrastructure to enable/disable typing rules

Author: sipma

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

CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml

@@ -31,6 +31,7 @@ open CHUtils
 
 (* chutil *)
 open CHLogger
+open CHXmlDocument
 
 (* bchlib *)
 open BCHBCTypePretty
@@ -72,6 +73,8 @@ object (self)
   (* constraints that involve a global variable *)
   val gvartypes = H.create 5
 
+  val rules_applied = H.create 5
+
   method reset =
     begin
       H.clear store;
@@ -81,9 +84,28 @@ object (self)
       H.clear gvartypes
     end
 
-  method add_constraint (c: type_constraint_t) =
+  method private add_rule_applied
+                   (faddr: string)
+                   (loc: string)
+                   (rule: string)
+                   (ix: int) =
+    let tir = {
+        tir_faddr = faddr;
+        tir_loc = loc;
+        tir_rule = rule;
+        tir_constraint_ix = ix
+      } in
+    let entry =
+      if H.mem rules_applied faddr then
+        H.find rules_applied faddr
+      else
+        [] in
+    H.replace rules_applied faddr (tir :: entry)
+
+  method add_constraint
+           (faddr: string) (loc: string) (rule: string) (c: type_constraint_t) =
     let index = tcd#index_type_constraint c in
-    (* index the constraint *)
+    let _ = self#add_rule_applied faddr loc rule index in
     if H.mem store index then
       ()
     else
@@ -188,33 +210,50 @@ object (self)
       if H.mem iaddrentry iaddr then H.find iaddrentry iaddr else [] in
     H.replace iaddrentry iaddr (c :: entry)
 
-  method add_var_constraint (tyvar: type_variable_t) =
-    self#add_constraint (TyVar (TyVariable tyvar))
+  method add_var_constraint
+           (faddr: string)
+           (loc: string)
+           (rule: string)
+           (tyvar: type_variable_t) =
+    self#add_constraint faddr loc rule (TyVar (TyVariable tyvar))
 
-  method add_term_constraint (t: type_term_t) =
+  method add_term_constraint
+           (faddr: string)
+           (loc: string)
+           (rule: string)
+           (t: type_term_t) =
     match t with
-    | TyVariable tv -> self#add_var_constraint tv
+    | TyVariable tv -> self#add_var_constraint faddr loc rule tv
     | _ -> ()
 
+  (*
   method add_zerocheck_constraint (tyvar: type_variable_t) =
     begin
       self#add_var_constraint tyvar;
       self#add_constraint (TyZeroCheck (TyVariable tyvar))
     end
+   *)
 
-  method add_subtype_constraint (t1: type_term_t) (t2: type_term_t) =
+  method add_subtype_constraint
+           (faddr: string)
+           (loc: string)
+           (rule: string)
+           (t1: type_term_t)
+           (t2: type_term_t) =
     begin
-      self#add_term_constraint t1;
-      self#add_term_constraint t2;
-      self#add_constraint (TySub (t1, t2))
+      self#add_term_constraint faddr loc rule t1;
+      self#add_term_constraint faddr loc rule t2;
+      self#add_constraint faddr loc rule (TySub (t1, t2))
     end
 
+  (*
   method add_ground_constraint (t1: type_term_t) (t2: type_term_t) =
     begin
       self#add_term_constraint t1;
       self#add_term_constraint t2;
       self#add_constraint (TyGround (t1, t2))
     end
+   *)
 
   method get_function_type_constraints (faddr: string): type_constraint_t list =
     if H.mem functiontypes faddr then
@@ -704,6 +743,31 @@ object (self)
         () in
     !result
 
+  method private write_xml_rules_applied (node: xml_element_int) =
+    let ranode = xmlElement "rules-applied" in
+    begin
+      H.iter (fun faddr rules ->
+          let fnode = xmlElement "function" in
+          let _ = fnode#setAttribute "faddr" faddr in
+          begin
+            List.iter (fun rule ->
+                let rnode = xmlElement "rule" in
+                begin
+                  rnode#setAttribute "loc" rule.tir_loc;
+                  rnode#setAttribute "rule" rule.tir_rule;
+                  rnode#setIntAttribute "tc-ix" rule.tir_constraint_ix;
+                  fnode#appendChildren [rnode]
+                end) rules;
+            ranode#appendChildren [fnode]
+          end) rules_applied;
+      node#appendChildren [ranode]
+    end
+
+  method write_xml (node: xml_element_int) =
+    begin
+      self#write_xml_rules_applied (node)
+    end
+
   method toPretty =
     let constraints = ref [] in
     let _ =