CHB: remove recording of return values and side effects

Author: sipma

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -406,12 +406,12 @@ object (self)
   (* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
    *                                                           return values *
    * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
-
+(*
   method record_return_value =
     let eax = self#env#mk_cpu_register_variable Eax in
     let returnExpr = self#rewrite_variable_to_external eax in
     self#f#record_return_value self#cia returnExpr
-
+ *)
 
   (* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
    *                                                            call targets *

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -59,7 +59,6 @@ open BCHConstantDefinitions
 open BCHCppClass
 open BCHCStruct
 open BCHDoubleword
-open BCHExternalPredicate
 open BCHFtsParameter
 open BCHFunctionInterface
 open BCHFunctionData
@@ -1561,8 +1560,7 @@ object (self)
 
   val instrbytes = H.create 5
   val jump_targets = H.create 5                           (* to be saved *)
-  val return_values = H.create 3
-  val sideeffects = H.create 3  (* iaddr -> sideeffect-ix *)
+
   val mutable nonreturning = false
   val mutable user_summary = None     (* to be deprecated *)
   val mutable appsummary =
@@ -1819,47 +1817,6 @@ object (self)
                 LBLOCK l ; NL ;
 		STR (string_repeat "~" 80) ; NL]
 
-  (* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
-   * record return values                                                    *
-   * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
-
-  method record_return_value (iaddr:ctxt_iaddress_t) (x:xpr_t) =
-    H.replace return_values iaddr x
-
-  method get_return_values = H.fold (fun _ x a -> x :: a) return_values []
-
-  method return_values_to_pretty =
-    let p = ref [] in
-    let _ = H.iter (fun iaddr x ->
-      let pp = LBLOCK [ STR iaddr ; STR ": " ; pr_expr x ; NL ] in
-      p := pp :: !p ) return_values in
-    LBLOCK [ STR "Return values: (" ; INT (H.length return_values) ; STR ")" ; NL ;
-	     INDENT (3, LBLOCK !p) ; NL ]
-
-  (* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
-   * record side effects                                                     *
-   * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
-
-  method record_sideeffect (iaddr: ctxt_iaddress_t) (s: xxpredicate_t) =
-    let index = id#index_xxpredicate s in
-    if H.mem sideeffects iaddr then
-      let prev_ix = H.find sideeffects iaddr in
-      if index = prev_ix then
-        ()
-      else
-        begin
-          H.replace sideeffects iaddr index;
-          sideeffects_changed <- true
-        end
-    else
-      begin
-        H.add sideeffects iaddr index;
-        sideeffects_changed <- true;
-        chlog#add
-          "sideeffects changed"
-          (LBLOCK [self#a#toPretty; STR ": "; xxpredicate_to_pretty s])
-      end
-
   method set_nonreturning =
     if nonreturning then () else
       let fa = self#get_address in

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -5274,13 +5274,6 @@ object
   (** Declares that this function is non-returning.*)
   method set_nonreturning: unit
 
-  (** [finfo#record_return_value iaddr xpr] records that the function
-      returns value [xpr] at return instruction [iaddr].*)
-  method record_return_value: ctxt_iaddress_t -> xpr_t -> unit
-
-  (** Returns the function return values recorded for this function.*)
-  method get_return_values: xpr_t list
-
 
   (* method set_dynlib_stub: call_target_t -> unit *)
 
@@ -5393,18 +5386,6 @@ object
   method set_unknown_java_native_method_signature: unit
 
 
-  (** {2 Side effects}*)
-
-  (** [finfo#record_sideeffect iaddr se] records side effect [se] (i.e.,
-      an effect that is observable outside of the function, such as writing
-      through a pointer provided as argument) at instruction address [iaddr].
-
-      This method is currently called only when an assignment is performed
-      with a left-hand-side that is an external memory reference.
-   *)
-  method record_sideeffect: ctxt_iaddress_t -> xxpredicate_t -> unit
-
-
   (** {1 Condition codes}
       The function info keeps track of test expressions and the variables used
       therein for conditional jump instructions. These methods are used mainly
@@ -5577,7 +5558,7 @@ object
   method summary_to_pretty: pretty_t
   method saved_registers_to_pretty: pretty_t
   method base_pointers_to_pretty: pretty_t
-  method return_values_to_pretty: pretty_t
+                                    (* method return_values_to_pretty: pretty_t *)
 
 end
 
@@ -5892,10 +5873,6 @@ class type floc_int =
 
     (** {1 Function summary}*)
 
-    (* evaluates the value of eax at this location and reports it to the function
-       info *)
-    method record_return_value: unit
-
     method evaluate_summary_address_term: bterm_t -> variable_t option
 
     method evaluate_summary_term: bterm_t -> variable_t -> xpr_t

CodeHawk/CHB/bchlibx86/bCHTranslateToCHIF.ml

@@ -2000,8 +2000,6 @@ let translate_instruction
 
   (* different control flow *)
   | RepzRet | Ret _ | BndRet _ ->
-     let floc = get_floc loc in
-     let _ = floc#record_return_value in
      let transaction =
        package_transaction finfo block_label (commands @ [invariantOperation]) in
      let nodes = [(block_label, [transaction])] in