diff options
| -rw-r--r-- | cfrontend/Cexec.v | 71 | ||||
| -rw-r--r-- | common/Events.v | 13 | ||||
| -rw-r--r-- | driver/Interp.ml | 58 | ||||
| -rw-r--r-- | driver/Interp_ext.ml | 121 | ||||
| -rw-r--r-- | extraction/extraction.v | 4 |
5 files changed, 82 insertions, 185 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 699c29e..36a62a8 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -387,19 +387,33 @@ Qed. (** External calls *) -Parameter do_external_function: ident -> signature -> list val -> mem -> option val. - -Axiom do_external_function_correct: - forall id sg (ge: genv) vargs m t vres m', - external_functions_sem id sg ge vargs m t vres m' <-> - do_external_function id sg vargs m = Some vres /\ t = E0 /\ m' = m. - -Definition do_ef_external (name: ident) (sg: signature) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match do_external_function name sg vargs m with - | None => None - | Some vres => Some(w, E0, vres, m) - end. +Variable do_external_function: + ident -> signature -> genv -> world -> list val -> mem -> option (world * trace * val * mem). + +Hypothesis do_external_function_sound: + forall id sg ge vargs m t vres m' w w', + do_external_function id sg ge w vargs m = Some(w', t, vres, m') -> + external_functions_sem id sg ge vargs m t vres m' /\ possible_trace w t w'. + +Hypothesis do_external_function_complete: + forall id sg ge vargs m t vres m' w w', + external_functions_sem id sg ge vargs m t vres m' -> + possible_trace w t w' -> + do_external_function id sg ge w vargs m = Some(w', t, vres, m'). + +Variable do_inline_assembly: + ident -> genv -> world -> list val -> mem -> option (world * trace * val * mem). + +Hypothesis do_inline_assembly_sound: + forall txt ge vargs m t vres m' w w', + do_inline_assembly txt ge w vargs m = Some(w', t, vres, m') -> + inline_assembly_sem txt ge vargs m t vres m' /\ possible_trace w t w'. + +Hypothesis do_inline_assembly_complete: + forall txt ge vargs m t vres m' w w', + inline_assembly_sem txt ge vargs m t vres m' -> + possible_trace w t w' -> + do_inline_assembly txt ge w vargs m = Some(w', t, vres, m'). Definition do_ef_volatile_load (chunk: memory_chunk) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := @@ -508,8 +522,8 @@ Definition do_ef_annot_val (text: ident) (targ: typ) Definition do_external (ef: external_function): world -> list val -> mem -> option (world * trace * val * mem) := match ef with - | EF_external name sg => do_ef_external name sg - | EF_builtin name sg => do_ef_external name sg + | EF_external name sg => do_external_function name sg ge + | EF_builtin name sg => do_external_function name sg ge | EF_vload chunk => do_ef_volatile_load chunk | EF_vstore chunk => do_ef_volatile_store chunk | EF_vload_global chunk id ofs => do_ef_volatile_load_global chunk id ofs @@ -519,7 +533,7 @@ Definition do_external (ef: external_function): | EF_memcpy sz al => do_ef_memcpy sz al | EF_annot text targs => do_ef_annot text targs | EF_annot_val text targ => do_ef_annot_val text targ - | EF_inline_asm text => do_ef_annot text nil + | EF_inline_asm text => do_inline_assembly text ge end. Lemma do_ef_external_sound: @@ -528,11 +542,6 @@ Lemma do_ef_external_sound: external_call ef ge vargs m t vres m' /\ possible_trace w t w'. Proof with try congruence. intros until m'. - assert (EXT: forall name sg, - do_ef_external name sg w vargs m = Some(w', t, vres, m') -> - external_functions_sem name sg ge vargs m t vres m' /\ possible_trace w t w'). - intros until sg. unfold do_ef_external. mydestr. - split. rewrite do_external_function_correct. auto. constructor. assert (VLOAD: forall chunk vargs, do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') -> @@ -552,9 +561,9 @@ Proof with try congruence. destruct ef; simpl. (* EF_external *) - auto. + eapply do_external_function_sound; eauto. (* EF_builtin *) - auto. + eapply do_external_function_sound; eauto. (* EF_vload *) auto. (* EF_vstore *) @@ -588,10 +597,7 @@ Proof with try congruence. split. constructor. apply eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. (* EF_inline_asm *) - unfold do_ef_annot. destruct vargs; simpl... mydestr. - split. change (Event_annot text nil) with (Event_annot text (annot_eventvals nil nil)). - constructor. constructor. - econstructor. constructor; eauto. constructor. + eapply do_inline_assembly_sound; eauto. Qed. Lemma do_ef_external_complete: @@ -600,11 +606,6 @@ Lemma do_ef_external_complete: do_external ef w vargs m = Some(w', t, vres, m'). Proof. intros. - assert (EXT: forall name sg, - external_functions_sem name sg ge vargs m t vres m' -> - do_ef_external name sg w vargs m = Some (w', t, vres, m')). - intros. rewrite do_external_function_correct in H1. destruct H1 as (A & B & C). - subst. unfold do_ef_external. rewrite A. inv H0. auto. assert (VLOAD: forall chunk vargs, volatile_load_sem chunk ge vargs m t vres m' -> @@ -620,9 +621,9 @@ Proof. destruct ef; simpl in *. (* EF_external *) - auto. + eapply do_external_function_complete; eauto. (* EF_builtin *) - auto. + eapply do_external_function_complete; eauto. (* EF_vload *) auto. (* EF_vstore *) @@ -650,7 +651,7 @@ Proof. inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. rewrite (eventval_of_val_complete _ _ _ H1). auto. (* EF_inline_asm *) - inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. inv H1. simpl. auto. + eapply do_inline_assembly_complete; eauto. Qed. (** * Reduction of expressions *) diff --git a/common/Events.v b/common/Events.v index 240af95..74c672e 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1446,7 +1446,7 @@ Qed. (** ** Semantics of external functions. *) (** For functions defined outside the program ([EF_external] and [EF_builtin]), - we simply axiomatize their semantics as a predicate that satisfies + we do not define their semantics, but only assume that it satisfies [extcall_properties]. *) Parameter external_functions_sem: ident -> signature -> extcall_sem. @@ -1454,6 +1454,13 @@ Parameter external_functions_sem: ident -> signature -> extcall_sem. Axiom external_functions_properties: forall id sg, extcall_properties (external_functions_sem id sg) sg. +(** We treat inline assembly similarly. *) + +Parameter inline_assembly_sem: ident -> extcall_sem. + +Axiom inline_assembly_properties: + forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None). + (** ** Combined semantics of external calls *) (** Combining the semantics given above for the various kinds of external calls, @@ -1480,7 +1487,7 @@ Definition external_call (ef: external_function): extcall_sem := | EF_memcpy sz al => extcall_memcpy_sem sz al | EF_annot txt targs => extcall_annot_sem txt targs | EF_annot_val txt targ=> extcall_annot_val_sem txt targ - | EF_inline_asm txt => extcall_annot_sem txt nil + | EF_inline_asm txt => inline_assembly_sem txt end. Theorem external_call_spec: @@ -1499,7 +1506,7 @@ Proof. apply extcall_memcpy_ok. apply extcall_annot_ok. apply extcall_annot_val_ok. - apply extcall_annot_ok. + apply inline_assembly_properties. Qed. Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). diff --git a/driver/Interp.ml b/driver/Interp.ml index 4777900..5fcca0b 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -12,14 +12,11 @@ (* Interpreting CompCert C sources *) -type caml_float = float - open Format open Camlcoq open Datatypes open AST open Integers -open Floats open Values open Memory open Globalenvs @@ -281,12 +278,12 @@ let rec purge_seen nextblock seen = (* Extract a string from a global pointer *) -let extract_string ge m id ofs = +let extract_string m blk ofs = let b = Buffer.create 80 in let rec extract blk ofs = - match Memory.Mem.load Mint8unsigned m blk ofs with + match Mem.load Mint8unsigned m blk ofs with | Some(Vint n) -> - let c = Char.chr (Int32.to_int (camlint_of_coqint n)) in + let c = Char.chr (Z.to_int n) in if c = '\000' then begin Some(Buffer.contents b) end else begin @@ -295,9 +292,7 @@ let extract_string ge m id ofs = end | _ -> None in - match Genv.find_symbol ge id with - | None -> None - | Some blk -> extract blk ofs + extract blk ofs (* Emulation of printf *) @@ -306,14 +301,14 @@ let extract_string ge m id ofs = let re_conversion = Str.regexp "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\|ll\\)?\\([aAcdeEfgGinopsuxX%]\\)" -external format_float: string -> caml_float -> string +external format_float: string -> float -> string = "caml_format_float" external format_int32: string -> int32 -> string = "caml_int32_format" external format_int64: string -> int64 -> string = "caml_int64_format" -let do_printf ge m fmt args = +let do_printf m fmt args = let b = Buffer.create 80 in let len = String.length fmt in @@ -339,24 +334,24 @@ let do_printf ge m fmt args = | [], _ -> Buffer.add_string b "<missing argument>"; scan pos' [] - | EVint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') -> + | Vint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') -> Buffer.add_string b (format_int32 pat (camlint_of_coqint i)); scan pos' args' - | EVfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') -> + | Vfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') -> Buffer.add_string b (format_float pat (camlfloat_of_coqfloat f)); scan pos' args' - | EVlong i :: args', ('d'|'i'|'u'|'o'|'x'|'X') -> + | Vlong i :: args', ('d'|'i'|'u'|'o'|'x'|'X') -> let pat = Str.replace_first (Str.regexp "ll") "" pat in Buffer.add_string b (format_int64 pat (camlint64_of_coqint i)); scan pos' args' - | EVptr_global(id, ofs) :: args', 's' -> + | Vptr(blk, ofs) :: args', 's' -> Buffer.add_string b - (match extract_string ge m id ofs with + (match extract_string m blk ofs with | Some s -> s | None -> "<bad string>"); scan pos' args' - | EVptr_global(id, ofs) :: args', 'p' -> - Printf.bprintf b "<&%s%+ld>" (extern_atom id) (camlint_of_coqint ofs); + | Vptr(blk, ofs) :: args', 'p' -> + Printf.bprintf b "<%ld%+ld>" (P.to_int32 blk) (camlint_of_coqint ofs); scan pos' args' | _ :: args', _ -> Buffer.add_string b "<formatting error>"; @@ -364,10 +359,29 @@ let do_printf ge m fmt args = end in scan 0 args; Buffer.contents b -(* Implementing external functions producing observable events *) +(* Implementation of external functions *) + +let re_stub = Str.regexp "\\$[ifl]*$" + +let chop_stub name = Str.replace_first re_stub "" name let (>>=) opt f = match opt with None -> None | Some arg -> f arg +let do_external_function id sg ge w args m = + match chop_stub(extern_atom id), args with + | "printf", Vptr(b, ofs) :: args' -> + extract_string m b ofs >>= fun fmt -> + print_string (do_printf m fmt args'); + flush stdout; + Cexec.list_eventval_of_val ge args sg.sig_args >>= fun eargs -> + Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) + | _ -> + None + +let do_inline_assembly txt ge w args m = None + +(* Implementing external functions producing observable events *) + let rec world ge m = Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m) @@ -388,7 +402,7 @@ and world_vstore ge m chunk id ofs ev = let do_event p ge time w ev = if !trace >= 1 then - fprintf p "@[<hov 2>Time %d: observable event: %a@]@." + fprintf p "@[<hov 2>Time %d: observable event:@ @[<hov 2>%a@]@]@." time print_event ev; (* Return new world after external action *) match ev with @@ -429,7 +443,7 @@ let diagnose_stuck_expr p ge w f a kont e m = | 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 w k a m in + let l = Cexec.step_expr ge do_external_function do_inline_assembly e w k a m in if List.exists (fun (ctx,red) -> red = Cexec.Stuckred) l then begin PrintCsyntax.print_pointer_hook := print_pointer ge e; fprintf p "@[<hov 2>Stuck subexpression:@ %a@]@." @@ -464,7 +478,7 @@ let do_step p prog ge time (s, w) = | First | Random -> exit (Int32.to_int (camlint_of_coqint r)) end | None -> - let l = Cexec.do_step ge w s in + let l = Cexec.do_step ge do_external_function do_inline_assembly w s in if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin pp_set_max_boxes p 1000; fprintf p "@[<hov 2>Stuck state: %a@]@." print_state (prog, ge, s); diff --git a/driver/Interp_ext.ml b/driver/Interp_ext.ml deleted file mode 100644 index 2fc12b8..0000000 --- a/driver/Interp_ext.ml +++ /dev/null @@ -1,121 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Implementing external functions for the reference interpreter. - The only such function currently implemented is "printf". *) - -open Format -open Camlcoq -open AST -open Values -open Memory - -(* Extract a string from a global pointer *) - -let extract_string m blk ofs = - let b = Buffer.create 80 in - let rec extract blk ofs = - match Mem.load Mint8unsigned m blk ofs with - | Some(Vint n) -> - let c = Char.chr (Z.to_int n) in - if c = '\000' then begin - Some(Buffer.contents b) - end else begin - Buffer.add_char b c; - extract blk (Z.succ ofs) - end - | _ -> - None in - extract blk ofs - -(* Emulation of printf *) - -(* All ISO C 99 formats except size modifier [L] (long double) *) - -let re_conversion = Str.regexp - "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\|ll\\)?\\([aAcdeEfgGinopsuxX%]\\)" - -external format_float: string -> float -> string - = "caml_format_float" -external format_int32: string -> int32 -> string - = "caml_int32_format" -external format_int64: string -> int64 -> string - = "caml_int64_format" - -let do_printf m fmt args = - - let b = Buffer.create 80 in - let len = String.length fmt in - - let opt_search_forward pos = - try Some(Str.search_forward re_conversion fmt pos) - with Not_found -> None in - - let rec scan pos args = - if pos < len then begin - match opt_search_forward pos with - | None -> - Buffer.add_substring b fmt pos (len - pos) - | Some pos1 -> - Buffer.add_substring b fmt pos (pos1 - pos); - let pat = Str.matched_string fmt - and conv = Str.matched_group 3 fmt - and pos' = Str.match_end() in - match args, conv.[0] with - | _, '%' -> - Buffer.add_char b '%'; - scan pos' args - | [], _ -> - Buffer.add_string b "<missing argument>"; - scan pos' [] - | Vint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') -> - Buffer.add_string b (format_int32 pat (camlint_of_coqint i)); - scan pos' args' - | Vfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') -> - Buffer.add_string b (format_float pat (camlfloat_of_coqfloat f)); - scan pos' args' - | Vlong i :: args', ('d'|'i'|'u'|'o'|'x'|'X') -> - let pat = Str.replace_first (Str.regexp "ll") "" pat in - Buffer.add_string b (format_int64 pat (camlint64_of_coqint i)); - scan pos' args' - | Vptr(blk, ofs) :: args', 's' -> - Buffer.add_string b - (match extract_string m blk ofs with - | Some s -> s - | None -> "<bad string>"); - scan pos' args' - | Vptr(blk, ofs) :: args', 'p' -> - Printf.bprintf b "<%ld%+ld>" (P.to_int32 blk) (camlint_of_coqint ofs); - scan pos' args' - | _ :: args', _ -> - Buffer.add_string b "<formatting error>"; - scan pos' args' - end - in scan 0 args; Buffer.contents b - -(* Implementation of external functions *) - -let re_stub = Str.regexp "\\$[ifl]*$" - -let chop_stub name = Str.replace_first re_stub "" name - -let do_external_function id sg args m = - match chop_stub(extern_atom id), args with - | "printf", Vptr(b, ofs) :: args' -> - begin match extract_string m b ofs with - | Some fmt -> print_string (do_printf m fmt args') - | None -> print_string "<bad printf>\n" - end; - flush stdout; - Some Vundef - | _ -> - None diff --git a/extraction/extraction.v b/extraction/extraction.v index 34e6b0a..047a9b4 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -23,7 +23,6 @@ Require Constprop. Require Tailcall. Require Allocation. Require Compiler. -Require Cexec. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -107,9 +106,6 @@ Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) -(* Reference interpreter *) -Extract Constant Cexec.do_external_function => "Interp_ext.do_external_function". - (* Processor-specific extraction directives *) Load extractionMachdep. |