diff options
| -rw-r--r-- | cparser/Cutil.ml | 2 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 2 | ||||
| -rw-r--r-- | cparser/StructReturn.ml | 5 | ||||
| -rw-r--r-- | driver/Interp.ml | 50 |
4 files changed, 52 insertions, 7 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index a3cb609..eb3f063 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 051fafb..3c39b99 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 2a4bbc1..57246ce 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 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 -> () |