From 0be44be49c5be412a9d23e37c7b4554a9049ecbe Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Nov 2013 16:18:46 +0000 Subject: Revised modeling of external functions and built-in functions: just axiomatize them. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2369 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cexec.v | 35 ++++++------ common/Events.v | 139 +++++++++--------------------------------------- driver/Interp.ml | 23 ++------ driver/Interp_ext.ml | 121 +++++++++++++++++++++++++++++++++++++++++ extraction/extraction.v | 4 ++ 5 files changed, 171 insertions(+), 151 deletions(-) create mode 100644 driver/Interp_ext.ml diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 03cab54..699c29e 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -385,16 +385,20 @@ Proof. elim n. red; tauto. Qed. -(** System calls and library functions *) +(** 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) := - do args <- list_eventval_of_val vargs (sig_args sg); - match nextworld_io w name args with + match do_external_function name sg vargs m with | None => None - | Some(res, w') => - do vres <- val_of_eventval res (proj_sig_res sg); - Some(w', Event_syscall name args res :: E0, vres, m) + | Some vres => Some(w, E0, vres, m) end. Definition do_ef_volatile_load (chunk: memory_chunk) @@ -524,13 +528,11 @@ 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 (IO: forall name sg, + assert (EXT: forall name sg, do_ef_external name sg w vargs m = Some(w', t, vres, m') -> - extcall_io_sem name sg ge vargs m t vres m' /\ possible_trace w t w'). - intros until sg. unfold do_ef_external. mydestr. destruct p as [res w'']; mydestr. - split. econstructor. apply list_eventval_of_val_sound; auto. - apply val_of_eventval_sound; auto. - econstructor. constructor; eauto. constructor. + 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') -> @@ -598,12 +600,11 @@ Lemma do_ef_external_complete: do_external ef w vargs m = Some(w', t, vres, m'). Proof. intros. - assert (IO: forall name sg, - extcall_io_sem name sg ge vargs m t vres m' -> + 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. inv H1. inv H0. inv H8. inv H6. - unfold do_ef_external. rewrite (list_eventval_of_val_complete _ _ _ H2). rewrite H8. - rewrite (val_of_eventval_complete _ _ _ H3). auto. + 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' -> diff --git a/common/Events.v b/common/Events.v index 3082503..240af95 100644 --- a/common/Events.v +++ b/common/Events.v @@ -606,12 +606,6 @@ Record extcall_properties (sem: extcall_sem) sem F V ge vargs m1 t vres m2 -> Val.has_type vres (proj_sig_res sg); -(** The number of arguments of an external call must agree with its signature. *) - ec_arity: - forall F V (ge: Genv.t F V) vargs m1 t vres m2, - sem F V ge vargs m1 t vres m2 -> - List.length vargs = List.length sg.(sig_args); - (** The semantics is invariant under change of global environment that preserves symbols. *) ec_symbols_preserved: forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) vargs m1 t vres m2, @@ -776,8 +770,6 @@ Proof. (* well typed *) unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. eapply Mem.load_type; eauto. -(* arity *) - inv H; inv H0; auto. (* symbols *) inv H1. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) @@ -840,8 +832,6 @@ Proof. (* well typed *) unfold proj_sig_res; simpl. inv H. inv H1. apply Val.load_result_type. eapply Mem.load_type; eauto. -(* arity *) - inv H; inv H1; auto. (* symbols *) inv H1. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. (* valid blocks *) @@ -989,8 +979,6 @@ Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H; constructor. -(* arity *) - inv H; simpl; auto. (* symbols preserved *) inv H1. constructor. eapply volatile_store_preserved; eauto. (* valid block *) @@ -1046,8 +1034,6 @@ Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H; constructor. -(* arity *) - inv H; simpl; auto. (* symbols preserved *) inv H1. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. (* valid block *) @@ -1110,8 +1096,6 @@ Proof. constructor; intros. (* well typed *) inv H. unfold proj_sig_res; simpl. auto. -(* arity *) - inv H. auto. (* symbols preserved *) inv H1; econstructor; eauto. (* valid block *) @@ -1173,30 +1157,9 @@ Lemma extcall_free_ok: extcall_properties extcall_free_sem (mksignature (Tint :: nil) None). Proof. -(* - assert (UNCHANGED: - forall (P: block -> Z -> Prop) m b lo hi m', - Mem.free m b lo hi = Some m' -> - lo < hi -> - (forall b' ofs, P b' ofs -> b' <> b \/ ofs < lo \/ hi <= ofs) -> - mem_unchanged_on P m m'). - intros; split; intros. - split; intros. - eapply Mem.perm_free_1; eauto. - eapply Mem.perm_free_3; eauto. - rewrite <- H3. eapply Mem.load_free; eauto. - destruct (eq_block b0 b); auto. right. right. - apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) (lo, hi)). - red; intros. apply Intv.notin_range. simpl. exploit H1; eauto. intuition. - simpl; generalize (size_chunk_pos chunk); omega. - simpl; omega. -*) - constructor; intros. (* well typed *) inv H. unfold proj_sig_res. simpl. auto. -(* arity *) - inv H. auto. (* symbols preserved *) inv H1; econstructor; eauto. (* valid block *) @@ -1301,8 +1264,6 @@ Proof. intros. constructor. (* return type *) intros. inv H. constructor. -(* arity *) - intros. inv H. auto. (* change of globalenv *) intros. inv H1. econstructor; eauto. (* valid blocks *) @@ -1383,62 +1344,6 @@ Proof. intros; inv H; inv H0. split. constructor. intros; split; congruence. Qed. -(** ** Semantics of system calls. *) - -Inductive extcall_io_sem (name: ident) (sg: signature) (F V: Type) (ge: Genv.t F V): - list val -> mem -> trace -> val -> mem -> Prop := - | extcall_io_sem_intro: forall vargs m args res vres, - eventval_list_match ge args (sig_args sg) vargs -> - eventval_match ge res (proj_sig_res sg) vres -> - extcall_io_sem name sg ge vargs m (Event_syscall name args res :: E0) vres m. - -Lemma extcall_io_ok: - forall name sg, - extcall_properties (extcall_io_sem name sg) sg. -Proof. - intros; constructor; intros. -(* well typed *) - inv H. eapply eventval_match_type; eauto. -(* arity *) - inv H. eapply eventval_list_match_length; eauto. -(* symbols preserved *) - inv H1. econstructor; eauto. - eapply eventval_list_match_preserved; eauto. - eapply eventval_match_preserved; eauto. -(* valid block *) - inv H; auto. -(* perms *) - inv H; auto. -(* readonly *) - inv H; auto. -(* mem extends *) - inv H. - exists vres; exists m1'; intuition. - econstructor; eauto. - eapply eventval_list_match_lessdef; eauto. -(* mem injects *) - inv H0. - exists f; exists vres; exists m1'; intuition. - econstructor; eauto. - eapply eventval_list_match_inject; eauto. - eapply eventval_match_inject_2; eauto. - red; intros; congruence. -(* trace length *) - inv H; simpl; omega. -(* receptive *) - inv H; inv H0. - exploit eventval_match_receptive; eauto. intros [v' EVM]. - exists v'; exists m1. econstructor; eauto. -(* determ *) - inv H; inv H0. - assert (args = args0). eapply eventval_list_match_determ_2; eauto. subst args0. - split. constructor. - eapply eventval_match_valid; eauto. - eapply eventval_match_valid; eauto. - eapply eventval_match_same_type; eauto. - intros EQ; inv EQ. split; auto. eapply eventval_match_determ_1; eauto. -Qed. - (** ** Semantics of annotations. *) Fixpoint annot_eventvals (targs: list annot_arg) (vargs: list eventval) : list eventval := @@ -1463,8 +1368,6 @@ Proof. intros; constructor; intros. (* well typed *) inv H. simpl. auto. -(* arity *) - inv H. simpl. eapply eventval_list_match_length; eauto. (* symbols *) inv H1. econstructor; eauto. eapply eventval_list_match_preserved; eauto. @@ -1507,41 +1410,50 @@ Lemma extcall_annot_val_ok: extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ)). Proof. intros; constructor; intros. - +(* well typed *) inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. - - inv H. auto. - +(* symbols *) inv H1. econstructor; eauto. eapply eventval_match_preserved; eauto. - +(* valid blocks *) inv H; auto. - +(* perms *) inv H; auto. - +(* readonly *) inv H; auto. - +(* mem extends *) inv H. inv H1. inv H6. exists v2; exists m1'; intuition. econstructor; eauto. eapply eventval_match_lessdef; eauto. - +(* mem inject *) inv H0. inv H2. inv H7. exists f; exists v'; exists m1'; intuition. econstructor; eauto. eapply eventval_match_inject; eauto. red; intros; congruence. - +(* trace length *) inv H; simpl; omega. - +(* receptive *) assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. - +(* determ *) inv H; inv H0. assert (arg = arg0). eapply eventval_match_determ_2; eauto. subst arg0. split. constructor. auto. 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 + [extcall_properties]. *) + +Parameter external_functions_sem: ident -> signature -> extcall_sem. + +Axiom external_functions_properties: + forall id sg, extcall_properties (external_functions_sem id sg) sg. + (** ** Combined semantics of external calls *) (** Combining the semantics given above for the various kinds of external calls, @@ -1557,8 +1469,8 @@ This predicate is used in the semantics of all CompCert languages. *) Definition external_call (ef: external_function): extcall_sem := match ef with - | EF_external name sg => extcall_io_sem name sg - | EF_builtin name sg => extcall_io_sem name sg + | EF_external name sg => external_functions_sem name sg + | EF_builtin name sg => external_functions_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk | EF_vload_global chunk id ofs => volatile_load_global_sem chunk id ofs @@ -1576,8 +1488,8 @@ Theorem external_call_spec: extcall_properties (external_call ef) (ef_sig ef). Proof. intros. unfold external_call, ef_sig. destruct ef. - apply extcall_io_ok. - apply extcall_io_ok. + apply external_functions_properties. + apply external_functions_properties. apply volatile_load_ok. apply volatile_store_ok. apply volatile_load_global_ok. @@ -1591,7 +1503,6 @@ Proof. Qed. Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). -Definition external_call_arity ef := ec_arity (external_call_spec ef). Definition external_call_symbols_preserved_gen ef := ec_symbols_preserved (external_call_spec ef). Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef). Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef). diff --git a/driver/Interp.ml b/driver/Interp.ml index 6f9336e..4777900 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -364,11 +364,7 @@ let do_printf ge m fmt args = end in scan 0 args; Buffer.contents b -(* Implementing external functions *) - -let re_stub = Str.regexp "\\$[ifl]*$" - -let chop_stub name = Str.replace_first re_stub "" name +(* Implementing external functions producing observable events *) let (>>=) opt f = match opt with None -> None | Some arg -> f arg @@ -376,17 +372,7 @@ let rec world ge m = Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m) and world_io ge m id args = - match chop_stub(extern_atom id), args with - | "printf", EVptr_global(id, ofs) :: args' -> - flush stderr; - begin match extract_string ge m id ofs with - | Some fmt -> print_string (do_printf ge m fmt args') - | None -> print_string "\n" - end; - flush stdout; - Some(EVint Integers.Int.zero, world ge m) - | _, _ -> - None + None and world_vload ge m chunk id ofs = Genv.find_symbol ge id >>= fun b -> @@ -567,8 +553,7 @@ let rec explore_all p prog ge seen queue = executing events. Volatile variables are turned into non-volatile ones, so that reads and writes can be performed. - Readonly variables are kept, for string literals in particular. - Writable variables are turned into empty vars, so that + Other variables are turned into empty vars, so that reads and writes just fail. Functions are preserved, although they are not used. *) @@ -579,8 +564,6 @@ let world_program prog = let gv' = if gv.gvar_volatile then {gv with gvar_readonly = false; gvar_volatile = false} - else if gv.gvar_readonly then - gv else {gv with gvar_init = []} in (id, Gvar gv') diff --git a/driver/Interp_ext.ml b/driver/Interp_ext.ml new file mode 100644 index 0000000..2fc12b8 --- /dev/null +++ b/driver/Interp_ext.ml @@ -0,0 +1,121 @@ +(* *********************************************************************) +(* *) +(* 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 ""; + 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 -> ""); + 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 ""; + 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 "\n" + end; + flush stdout; + Some Vundef + | _ -> + None diff --git a/extraction/extraction.v b/extraction/extraction.v index 047a9b4..34e6b0a 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -23,6 +23,7 @@ Require Constprop. Require Tailcall. Require Allocation. Require Compiler. +Require Cexec. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -106,6 +107,9 @@ 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. -- cgit v1.2.3