From d11cd6e87c635d843759d10f9173c1a28ff3c62b Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 19 Apr 2017 12:16:00 +0100
Subject: attempt to optimise performance if not tracing writes.

---
 src/gen_lib/sail_values.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index 600faddc..90eb69fe 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -2,8 +2,7 @@ open Big_int_Z
 open Printf
 
 let trace_writes = ref false
-let tracef : ('a, out_channel, unit) format -> 'a =
-  function f -> if !trace_writes then printf f else ifprintf stderr f
+let tracef = printf
 
 (* only expected to be 0, 1, 2; 2 represents undef *)
 type vbit = Vone | Vzero | Vundef
@@ -163,12 +162,14 @@ let get_register_field_bit reg field =
 let set_register register value = match register,value with
   | Vregister(a,_,_,name,_), Vregister(new_v,_,_,_,_) -> 
      begin
-       tracef "%s <- %s\n" name (string_of_value value);
+       if !trace_writes then
+         tracef "%s <- %s\n" name (string_of_value value);
        a := !new_v
      end
   | Vregister(a,_,_,name,_), Vvector(new_v,_,_) ->
      begin
-       tracef "%s <- %s\n" name (string_of_value value);
+       if !trace_writes then
+         tracef "%s <- %s\n" name (string_of_value value);
        a := new_v
      end
   | _ -> failwith "set_register of non-register"
@@ -227,7 +228,8 @@ let set_register_field_v reg field new_v =
   match reg with
   | Vregister(array,start,dir,name,fields) ->
      begin
-       tracef "%s[%s] <- %s\n" name field (string_of_value new_v);
+       if !trace_writes then
+         tracef "%s[%s] <- %s\n" name field (string_of_value new_v);
     (match List.assoc field fields with
      | (i,j) ->
        if i = j
@@ -240,7 +242,8 @@ let set_register_field_bit reg field new_v =
   match reg with
   | Vregister(array,start,dir,name,fields) ->
      begin
-       tracef "%s.%s <- %s\n" name field (string_of_bit new_v);
+       if !trace_writes then
+         tracef "%s.%s <- %s\n" name field (string_of_bit new_v);
     (match List.assoc field fields with
      | (i,j) ->
        if i = j
-- 
cgit v1.2.3