summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-29 08:42:10 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-29 08:42:10 +0000
commitc42d68fdeeef7d08b64a900f52d6b295ad31f4f0 (patch)
treebe1575a8e04e814306d7fd3611071c6bc4599fe3
parent55a23ce430234a40081222a213c5bb6b157b7552 (diff)
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
-rw-r--r--cfrontend/PrintCsyntax.ml26
-rw-r--r--driver/Interp.ml54
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)