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

4 files changed, 52 insertions, 7 deletions

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index a3cb609c..eb3f0639 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -720,7 +720,7 @@ let nullconst =
 
 (* Construct a cast expression *)
 
-let ecast e ty = { edesc = ECast(ty, e); etyp = ty }
+let ecast ty e = { edesc = ECast(ty, e); etyp = ty }
 
 (* Construct an assignment expression *)
 
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 051fafb9..3c39b99a 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -171,6 +171,8 @@ val nullconst : exp
   (* Expression for [(void * ) 0] *)
 val eaddrof : exp -> exp
   (* Expression for [&e] *)
+val ecast : typ -> exp -> exp
+  (* Expression for [(ty)e] *)
 val eassign : exp -> exp -> exp
   (* Expression for [e1 = e2] *)
 val ecomma :  exp -> exp -> exp
diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml
index 2a4bbc19..57246ce1 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -65,10 +65,7 @@ let rec transf_expr env ctx e =
     when is_composite_type env ty ->
       transf_composite_call env ctx (Some lhs) fn args ty
   | EBinop(Ocomma, e1, e2, ty) ->
-      {edesc = EBinop(Ocomma, transf_expr env Effects e1,
-                              transf_expr env ctx e2,
-                              transf_type env ty);
-       etyp = newty}
+      ecomma (transf_expr env Effects e1) (transf_expr env ctx e2)
   | EBinop(op, e1, e2, ty) ->
       {edesc = EBinop(op, transf_expr env Val e1,
                           transf_expr env Val e2,
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 50e512b2..c97f4fa9 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 -> ()