summaryrefslogtreecommitdiff
path: root/driver
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-10 10:23:43 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-10 10:23:43 +0000
commit7cde5744d5fa12c76f46bcd180ecfe0b4d00afb8 (patch)
treeb11e9aa1e3c97c7c1e53e8eab298aa65e7c2e8c1 /driver
parent2594c23c95d22f838952b0b335231ba81a657b0d (diff)
Interp: help debug stuck expressions
StructReturn: was building an ill-typed Ecomma expression Cutil: export "ecast" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1816 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
-rw-r--r--driver/Interp.ml50
1 files changed, 48 insertions, 2 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 50e512b..c97f4fa 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -371,6 +371,50 @@ let do_event p ge time s ev =
let do_events p ge time s t =
List.iter (do_event p ge time s) t
+(* Debugging stuck expressions *)
+
+let (|||) a b = a || b (* strict boolean or *)
+
+let diagnose_stuck_expr p ge f a kont e m =
+ let rec diagnose k a =
+ (* diagnose subexpressions first *)
+ let found =
+ match k, a with
+ | LV, Ederef(r, ty) -> diagnose RV r
+ | LV, Efield(r, f, ty) -> diagnose RV r
+ | RV, Evalof(l, ty) -> diagnose LV l
+ | RV, Eaddrof(l, ty) -> diagnose LV l
+ | RV, Eunop(op, r1, ty) -> diagnose RV r1
+ | RV, Ebinop(op, r1, r2, ty) -> diagnose RV r1 ||| diagnose RV r2
+ | RV, Ecast(r1, ty) -> diagnose RV r1
+ | RV, Econdition(r1, r2, r3, ty) -> diagnose RV r1
+ | RV, Eassign(l1, r2, ty) -> diagnose LV l1 ||| diagnose RV r2
+ | RV, Eassignop(op, l1, r2, tyres, ty) -> diagnose LV l1 ||| diagnose RV r2
+ | RV, Epostincr(id, l, ty) -> diagnose LV l
+ | RV, Ecomma(r1, r2, ty) -> diagnose RV r1
+ | RV, Eparen(r1, ty) -> diagnose RV r1
+ | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs
+ | _, _ -> false in
+ 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
+ fprintf p "@[<hov 2>Stuck subexpression:@ %a@]@."
+ PrintCsyntax.print_expr a;
+ true
+ end else false
+ end
+
+ and diagnose_list al =
+ match al with
+ | Enil -> false
+ | Econs(a1, al') -> diagnose RV a1 ||| diagnose_list al'
+
+ in diagnose RV a
+
+let diagnose_stuck_state p ge = function
+ | ExprState(f,a,k,e,m) -> ignore(diagnose_stuck_expr p ge f a k e m)
+ | _ -> ()
+
(* Exploration *)
let do_step p prog ge time s =
@@ -388,8 +432,9 @@ let do_step p prog ge time s =
| None ->
let l = Cexec.do_step ge world s in
if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin
- if !trace = 1 then
- fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s;
+ pp_set_max_boxes p 1000;
+ fprintf p "@[<hov 2>Stuck state: %a@]@." (print_state prog) s;
+ diagnose_stuck_state p ge s;
fprintf p "ERROR: Undefined behavior@.";
fprintf p "@].";
exit 126
@@ -452,6 +497,7 @@ let fixup_main p =
let execute prog =
Random.self_init();
let p = err_formatter in
+ pp_set_max_indent p 30;
pp_set_max_boxes p 10;
match fixup_main prog with
| None -> ()