From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Clflags.ml | 4 +--- driver/Compiler.v | 13 +++++++++---- driver/Complements.v | 10 ++++++++-- driver/Driver.ml | 17 +++++------------ driver/Interp.ml | 36 ++++++++++++++++++++---------------- 5 files changed, 43 insertions(+), 37 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index cb26b72..95f4209 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -17,12 +17,10 @@ let linker_options = ref ([]: string list) let exe_name = ref "a.out" let option_flonglong = ref true let option_flongdouble = ref false -let option_fstruct_passing = ref false -let option_fstruct_assign = ref false +let option_fstruct_return = ref false let option_fbitfields = ref false let option_fvararg_calls = ref true let option_fpacked_structs = ref false -let option_fvolatile_rmw = ref true let option_fmadd = ref false let option_fsse = ref true let option_dparse = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index ce9db20..6779aaf 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -400,7 +400,7 @@ Theorem transf_cstrategy_program_correct: forall p tp, transf_c_program p = OK tp -> forward_simulation (Cstrategy.semantics p) (Asm.semantics tp) - * backward_simulation (Cstrategy.semantics p) (Asm.semantics tp). + * backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp). Proof. intros. assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)). @@ -411,8 +411,9 @@ Proof. exact (fst (transf_clight_program_correct _ _ EQ1)). split. auto. - apply forward_to_backward_simulation. auto. - apply Cstrategy.semantics_receptive. + apply forward_to_backward_simulation. + apply factor_forward_simulation. auto. eapply sd_traces. eapply Asm.semantics_determinate. + apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. apply Asm.semantics_determinate. Qed. @@ -422,7 +423,11 @@ Theorem transf_c_program_correct: backward_simulation (Csem.semantics p) (Asm.semantics tp). Proof. intros. - eapply compose_backward_simulation. + apply compose_backward_simulation with (atomic (Cstrategy.semantics p)). + eapply sd_traces; eapply Asm.semantics_determinate. + apply factor_backward_simulation. apply Cstrategy.strategy_simulation. + apply Csem.semantics_single_events. + eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive. exact (snd (transf_cstrategy_program_correct _ _ H)). Qed. diff --git a/driver/Complements.v b/driver/Complements.v index 1b7e974..57351a2 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -78,15 +78,21 @@ Theorem transf_cstrategy_program_preservation: program_behaves (Asm.semantics tp) beh -> program_behaves (Cstrategy.semantics p) beh). Proof. + assert (WBT: forall p, well_behaved_traces (Cstrategy.semantics p)). + intros. eapply ssr_well_behaved. apply Cstrategy.semantics_strongly_receptive. intros. intuition. eapply forward_simulation_behavior_improves; eauto. apply (fst (transf_cstrategy_program_correct _ _ H)). - eapply backward_simulation_behavior_improves; eauto. + exploit backward_simulation_behavior_improves. apply (snd (transf_cstrategy_program_correct _ _ H)). + eauto. + intros [beh1 [A B]]. exists beh1; split; auto. rewrite atomic_behaviors; auto. eapply forward_simulation_same_safe_behavior; eauto. apply (fst (transf_cstrategy_program_correct _ _ H)). - eapply backward_simulation_same_safe_behavior; eauto. + exploit backward_simulation_same_safe_behavior. apply (snd (transf_cstrategy_program_correct _ _ H)). + intros. rewrite <- atomic_behaviors in H2; eauto. eauto. + intros. rewrite atomic_behaviors; auto. Qed. (** We can also use the alternate big-step semantics for [Cstrategy] diff --git a/driver/Driver.ml b/driver/Driver.ml index cee6250..9813939 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -69,11 +69,9 @@ let parse_c_file sourcename ifile = (* Simplification options *) let simplifs = "b" (* blocks: mandatory *) - ^ (if !option_fstruct_passing then "s" else "") - ^ (if !option_fstruct_assign then "S" else "") + ^ (if !option_fstruct_return then "s" else "") ^ (if !option_fbitfields then "f" else "") ^ (if !option_fpacked_structs then "p" else "") - ^ (if !option_fvolatile_rmw then "v" else "") in (* Parsing and production of a simplified C AST *) let ast = @@ -333,10 +331,8 @@ Language support options (use -fno- to turn off -f) : -fbitfields Emulate bit fields in structs [off] -flonglong Partial emulation of 'long long' types [on] -flongdouble Treat 'long double' as 'double' [off] - -fstruct-passing Emulate passing structs and unions by value [off] - -fstruct-assign Emulate assignment between structs or unions [off] + -fstruct-return Emulate returning structs and unions by value [off] -fvararg-calls Emulate calls to variable-argument functions [on] - -fvolatile-rmw Emulate ++, -- and op= on volatile l-values [on] -fpacked-structs Emulate packed structs [off] -fall Activate all language support options above -fnone Turn off all language support options above @@ -374,9 +370,8 @@ Interpreter mode: " let language_support_options = [ - option_fbitfields; option_flonglong; option_flongdouble; option_fstruct_passing; - option_fstruct_assign; option_fvararg_calls; option_fpacked_structs; - option_fvolatile_rmw + option_fbitfields; option_flonglong; option_flongdouble; + option_fstruct_return; option_fvararg_calls; option_fpacked_structs ] let cmdline_actions = @@ -434,14 +429,12 @@ let cmdline_actions = ] @ f_opt "longlong" option_flonglong @ f_opt "longdouble" option_flongdouble - @ f_opt "struct-passing" option_fstruct_passing - @ f_opt "struct-assign" option_fstruct_assign + @ f_opt "struct-return" option_fstruct_return @ f_opt "bitfields" option_fbitfields @ f_opt "vararg-calls" option_fvararg_calls @ f_opt "madd" option_fmadd @ f_opt "packed-structs" option_fpacked_structs @ f_opt "sse" option_fsse - @ f_opt "volatile-rmw" option_fvolatile_rmw let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 }; 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 "@[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 "@[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) | _ -> -- cgit v1.2.3