Better printing of pointer values and of locations.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1830 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 54 insertions, 26 deletions

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 0616049..3880188 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -21,6 +21,7 @@ open Camlcoq
 open Datatypes
 open Values
 open AST
+open Globalenvs
 open Csyntax
 
 let name_unop = function
@@ -167,6 +168,17 @@ let rec precedence = function
 
 (* Expressions *)
 
+let print_pointer_hook
+   : (formatter -> Values.block * Integers.Int.int -> unit) ref
+   = ref (fun p (b, ofs) -> ())
+
+let print_value p v =
+  match v with
+  | Vint n -> fprintf p "%ld" (camlint_of_coqint n)
+  | Vfloat f -> fprintf p "%F" f
+  | Vptr(b, ofs) -> fprintf p "<ptr%a>" !print_pointer_hook (b, ofs)
+  | Vundef -> fprintf p "<undef>"
+
 let rec expr p (prec, e) =
   let (prec', assoc) = precedence e in
   let (prec1, prec2) =
@@ -177,8 +189,8 @@ let rec expr p (prec, e) =
   then fprintf p "@[<hov 2>("
   else fprintf p "@[<hov 2>";
   begin match e with
-  | Eloc _ ->
-      fprintf p "<loc>"
+  | Eloc(b, ofs, _) ->
+      fprintf p "<loc%a>" !print_pointer_hook (b, ofs)
   | Evar(id, _) ->
       fprintf p "%s" (extern_atom id)
   | Ederef(a1, _) ->
@@ -187,14 +199,8 @@ let rec expr p (prec, e) =
       fprintf p "%a.%s" expr (prec', a1) (extern_atom f)
   | Evalof(l, _) ->
       expr p (prec, l)
-  | Eval(Vint n, _) ->
-      fprintf p "%ld" (camlint_of_coqint n)
-  | Eval(Vfloat f, _) ->
-      fprintf p "%F" f
-  | Eval(Vptr _, _) ->
-      fprintf p "<ptr>"
-  | Eval(Vundef, _) ->
-      fprintf p "<undef>"
+  | Eval(v, _) ->
+      print_value p (v)
   | Esizeof(ty, _) ->
       fprintf p "sizeof(%s)" (name_type ty)
   | Ealignof(ty, _) ->
diff --git a/driver/Interp.ml b/driver/Interp.ml
index c97f4fa..62f3093 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -40,11 +40,16 @@ let random_volatiles = ref false
 
 (* Printing events *)
 
+let print_id_ofs p (id, ofs) =
+  let id = extern_atom id and ofs = camlint_of_coqint ofs in
+  if ofs = 0l
+  then fprintf p " %s" id
+  else fprintf p " %s%+ld" id ofs
+
 let print_eventval p = function
   | EVint n -> fprintf p "%ld" (camlint_of_coqint n)
   | EVfloat f -> fprintf p "%F" f
-  | EVptr_global(id, ofs) -> 
-      fprintf p "&%s%+ld" (extern_atom id) (camlint_of_coqint ofs)
+  | EVptr_global(id, ofs) -> fprintf p "&%a" print_id_ofs (id, ofs)
 
 let print_eventval_list p = function
   | [] -> ()
@@ -85,32 +90,47 @@ let name_of_fundef prog fd =
 let name_of_function prog fn =
   name_of_fundef prog (Internal fn)
 
-let print_val p = function
-  | Vint n -> fprintf p "%ld" (camlint_of_coqint n)
-  | Vfloat f -> fprintf p "%F" f
-  | Vptr(b, ofs) -> fprintf p "<ptr>"
-  | Vundef -> fprintf p "<undef>"
+let invert_local_variable e b =
+  Maps.PTree.fold 
+    (fun res id (b', _) -> if b = b' then Some id else res)
+    e None
+
+let print_pointer ge e p (b, ofs) =
+  match invert_local_variable e b with
+  | Some id -> print_id_ofs p (id, ofs)
+  | None ->
+      match Genv.invert_symbol ge b with
+      | Some id -> print_id_ofs p (id, ofs)
+      | None -> ()
+
+let print_val = PrintCsyntax.print_value
 
-let print_val_list p = function
+let print_val_list p vl =
+  match vl with
   | [] -> ()
   | v1 :: vl ->
       print_val p v1;
       List.iter (fun v -> fprintf p ",@ %a" print_val v) vl
 
-let print_state prog p = function
+let print_state p (prog, ge, s) =
+  match s with
   | State(f, s, k, e, m) ->
+      PrintCsyntax.print_pointer_hook := print_pointer ge e;
       fprintf p "in function %s, statement@ @[<hv 0>%a@]"
               (name_of_function prog f)
-              PrintCsyntax.print_stmt s 
+              PrintCsyntax.print_stmt s
   | ExprState(f, r, k, e, m) ->
+      PrintCsyntax.print_pointer_hook := print_pointer ge e;
       fprintf p "in function %s, expression@ @[<hv 0>%a@]"
               (name_of_function prog f)
               PrintCsyntax.print_expr r
   | Callstate(fd, args, k, m) ->
+      PrintCsyntax.print_pointer_hook := print_pointer ge Maps.PTree.empty;
       fprintf p "calling@ @[<hov 2>%s(%a)@]"
               (name_of_fundef prog fd)
               print_val_list args
   | Returnstate(res, k, m) ->
+      PrintCsyntax.print_pointer_hook := print_pointer ge Maps.PTree.empty;
       fprintf p "returning@ %a"
               print_val res
   | Stuckstate ->
@@ -398,6 +418,7 @@ let diagnose_stuck_expr p ge f a kont e m =
   if found then true else begin
     let l = Cexec.step_expr ge e world k a m in
     if List.exists (fun (ctx,red) -> red = Cexec.Stuckred) l then begin
+      PrintCsyntax.print_pointer_hook := print_pointer ge e;
       fprintf p "@[<hov 2>Stuck subexpression:@ %a@]@."
               PrintCsyntax.print_expr a;
       true
@@ -419,7 +440,7 @@ let diagnose_stuck_state p ge = function
 
 let do_step p prog ge time s =
   if !trace >= 2 then
-    fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s;
+    fprintf p "@[<hov 2>Time %d: %a@]@." time print_state (prog, ge, s);
   match Cexec.at_final_state s with
   | Some r ->
       if !trace >= 1 then begin
@@ -433,10 +454,9 @@ let do_step p prog ge time s =
       let l = Cexec.do_step ge world s in
       if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin
         pp_set_max_boxes p 1000;
-        fprintf p "@[<hov 2>Stuck state: %a@]@." (print_state prog) s;
+        fprintf p "@[<hov 2>Stuck state: %a@]@." print_state (prog, ge, s);
         diagnose_stuck_state p ge s;
         fprintf p "ERROR: Undefined behavior@.";
-        fprintf p "@].";
         exit 126
       end else begin
         List.iter (fun (t, s') -> do_events p ge time s t) l;
@@ -496,7 +516,7 @@ let fixup_main p =
 
 let execute prog =
   Random.self_init();
-  let p = err_formatter in
+  let p = std_formatter in
   pp_set_max_indent p 30;
   pp_set_max_boxes p 10;
   match fixup_main prog with
@@ -504,5 +524,7 @@ let execute prog =
   | Some prog1 ->
       let prog2 = if !random_volatiles then prog1 else unvolatile prog1 in
       match Cexec.do_initial_state prog2 with
-      | None -> fprintf p "ERROR: Initial state undefined@."
-      | Some(ge, s) -> explore p prog2 ge 0 (StateSet.singleton s)
+      | None ->
+          fprintf p "ERROR: Initial state undefined@."
+      | Some(ge, s) ->
+          explore p prog2 ge 0 (StateSet.singleton s)