diff options
Diffstat (limited to 'driver/Interp.ml')
| -rw-r--r-- | driver/Interp.ml | 36 |
1 files changed, 20 insertions, 16 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index a1e01f0..50e512b 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -113,12 +113,15 @@ let print_state prog p = function | Returnstate(res, k, m) -> fprintf p "returning@ %a" print_val res + | Stuckstate -> + fprintf p "stuck after an undefined expression" let mem_of_state = function | State(f, s, k, e, m) -> m | ExprState(f, r, k, e, m) -> m | Callstate(fd, args, k, m) -> m | Returnstate(res, k, m) -> m + | Stuckstate -> assert false (* Comparing memory states *) @@ -211,6 +214,7 @@ let rank_state = function | ExprState _ -> 1 | Callstate _ -> 2 | Returnstate _ -> 3 + | Stuckstate -> 4 let compare_state s1 s2 = if s1 == s2 then 0 else @@ -382,16 +386,17 @@ let do_step p prog ge time s = exit (Int32.to_int (camlint_of_coqint r)) end | None -> - match Cexec.do_step ge world s with - | [] -> - if !trace = 1 then - fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s; - fprintf p "ERROR: Undefined behavior@."; - fprintf p "@]."; - exit 126 - | l -> - List.iter (fun (t, s') -> do_events p ge time s t) l; - List.map snd l + 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; + 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; + List.map snd l + end let rec explore p prog ge time ss = let succs = @@ -415,14 +420,13 @@ let unvolatile prog = {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars} let change_main_function p old_main old_main_ty = - let tint = Tint(I32, Signed) in let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in - let arg1 = Eval(Vint(coqint_of_camlint 0l), tint) in + let arg1 = Eval(Vint(coqint_of_camlint 0l), type_int32s) in let arg2 = arg1 in let body = - Sreturn(Some(Ecall(old_main, Econs(arg1, Econs(arg2, Enil)), tint))) in + Sreturn(Some(Ecall(old_main, Econs(arg1, Econs(arg2, Enil)), type_int32s))) in let new_main_fn = - { fn_return = tint; fn_params = []; fn_vars = []; fn_body = body } in + { fn_return = type_int32s; fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in { p with prog_main = new_main_id; @@ -431,9 +435,9 @@ let change_main_function p old_main old_main_ty = let fixup_main p = try match type_of_fundef (List.assoc p.prog_main p.prog_funct) with - | Tfunction(Tnil, Tint(I32, Signed)) -> + | Tfunction(Tnil, Tint(I32, Signed, _)) -> Some p - | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_))), Tnil)), + | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)), Tint _) as ty -> Some (change_main_function p p.prog_main ty) | _ -> |