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

5 files changed, 171 insertions, 151 deletions

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 "<bad printf>\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 "<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 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.