Merge branch 'master' into dwarf

4 files changed, 249 insertions, 46 deletions

diff --git a/common/AST.v b/common/AST.v
index 9c29a374..d2926178 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -576,7 +576,7 @@ Inductive external_function : Type :=
          Produces no observable event. *)
   | EF_memcpy (sz: Z) (al: Z)
      (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *)
-  | EF_annot (text: ident) (targs: list annot_arg)
+  | EF_annot (text: ident) (targs: list typ)
      (** A programmer-supplied annotation.  Takes zero, one or several arguments,
          produces an event carrying the text and the values of these arguments,
          and returns no value. *)
@@ -584,27 +584,15 @@ Inductive external_function : Type :=
      (** Another form of annotation that takes one argument, produces
          an event carrying the text and the value of this argument,
          and returns the value of the argument. *)
-  | EF_inline_asm (text: ident)
+  | EF_inline_asm (text: ident).
      (** Inline [asm] statements.  Semantically, treated like an
          annotation with no parameters ([EF_annot text nil]).  To be
          used with caution, as it can invalidate the semantic
          preservation theorem.  Generated only if [-finline-asm] is
          given. *)
 
-with annot_arg : Type :=
-  | AA_arg (ty: typ)
-  | AA_int (n: int)
-  | AA_float (n: float).
-
 (** The type signature of an external function. *)
 
-Fixpoint annot_args_typ (targs: list annot_arg) : list typ :=
-  match targs with
-  | nil => nil
-  | AA_arg ty :: targs' => ty :: annot_args_typ targs'
-  | _ :: targs' => annot_args_typ targs'
-  end.
-
 Definition ef_sig (ef: external_function): signature :=
   match ef with
   | EF_external name sg => sg
@@ -616,7 +604,7 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default
   | EF_free => mksignature (Tint :: nil) None cc_default
   | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default
-  | EF_annot text targs => mksignature (annot_args_typ targs) None cc_default
+  | EF_annot text targs => mksignature targs None cc_default
   | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default
   | EF_inline_asm text => mksignature nil None cc_default
   end.
@@ -653,7 +641,7 @@ Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2}
 Proof.
   generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros.
   decide equality.
-  apply list_eq_dec. decide equality. apply Float.eq_dec. 
+  apply list_eq_dec. auto.
 Defined.
 Global Opaque external_function_eq.
 
@@ -699,3 +687,56 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
   end.
 
 End TRANSF_PARTIAL_FUNDEF.
+
+(** * Arguments to annotations *)
+
+Set Contextual Implicit. 
+
+Inductive annot_arg (A: Type) : Type :=
+  | AA_base (x: A)
+  | AA_int (n: int)
+  | AA_long (n: int64)
+  | AA_float (f: float)
+  | AA_single (f: float32)
+  | AA_loadstack (chunk: memory_chunk) (ofs: int)
+  | AA_addrstack (ofs: int)
+  | AA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int)
+  | AA_addrglobal (id: ident) (ofs: int)
+  | AA_longofwords (hi lo: annot_arg A).
+
+Fixpoint globals_of_annot_arg (A: Type) (a: annot_arg A) : list ident :=
+  match a with
+  | AA_loadglobal chunk id ofs => id :: nil
+  | AA_addrglobal id ofs => id :: nil
+  | AA_longofwords hi lo => globals_of_annot_arg hi ++ globals_of_annot_arg lo
+  | _ => nil
+  end.
+
+Definition globals_of_annot_args (A: Type) (al: list (annot_arg A)) : list ident :=
+  List.fold_right (fun a l => globals_of_annot_arg a ++ l) nil al.
+
+Fixpoint params_of_annot_arg (A: Type) (a: annot_arg A) : list A :=
+  match a with
+  | AA_base x => x :: nil
+  | AA_longofwords hi lo => params_of_annot_arg hi ++ params_of_annot_arg lo
+  | _ => nil
+  end.
+
+Definition params_of_annot_args (A: Type) (al: list (annot_arg A)) : list A :=
+  List.fold_right (fun a l => params_of_annot_arg a ++ l) nil al.
+
+Fixpoint map_annot_arg (A B: Type) (f: A -> B) (a: annot_arg A) : annot_arg B :=
+  match a with
+  | AA_base x => AA_base (f x)
+  | AA_int n => AA_int n
+  | AA_long n => AA_long n
+  | AA_float n => AA_float n
+  | AA_single n => AA_single n
+  | AA_loadstack chunk ofs => AA_loadstack chunk ofs
+  | AA_addrstack ofs => AA_addrstack ofs
+  | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs
+  | AA_addrglobal id ofs => AA_addrglobal id ofs
+  | AA_longofwords hi lo => 
+      AA_longofwords (map_annot_arg f hi) (map_annot_arg f lo)
+  end.
+
diff --git a/common/Events.v b/common/Events.v
index 3fb58806..15bf4e12 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1344,25 +1344,16 @@ Qed.
 
 (** ** Semantics of annotations. *)
 
-Fixpoint annot_eventvals (targs: list annot_arg) (vargs: list eventval) : list eventval :=
-  match targs, vargs with
-  | AA_arg ty :: targs', varg :: vargs' => varg :: annot_eventvals targs' vargs'
-  | AA_int n :: targs', _ => EVint n :: annot_eventvals targs' vargs
-  | AA_float n :: targs', _ => EVfloat n :: annot_eventvals targs' vargs
-  | _, _ => vargs
-  end.
-
-Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (ge: Senv.t):
+Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t):
               list val -> mem -> trace -> val -> mem -> Prop :=
   | extcall_annot_sem_intro: forall vargs m args,
-      eventval_list_match ge args (annot_args_typ targs) vargs ->
-      extcall_annot_sem text targs ge vargs m
-           (Event_annot text (annot_eventvals targs args) :: E0) Vundef m.
+      eventval_list_match ge args targs vargs ->
+      extcall_annot_sem text targs ge vargs m (Event_annot text args :: E0) Vundef m.
 
 Lemma extcall_annot_ok:
   forall text targs,
   extcall_properties (extcall_annot_sem text targs)
-                     (mksignature (annot_args_typ targs) None cc_default)
+                     (mksignature targs None cc_default)
                      nil.
 Proof.
   intros; constructor; intros.
@@ -1794,9 +1785,133 @@ Proof.
   split; congruence.
 Qed.
 
+(** * Evaluation of annotation arguments *)
+
+Section EVAL_ANNOT_ARG.
+
+Variable A: Type.
+Variable ge: Senv.t.
+Variable e: A -> val.
+Variable sp: val.
+Variable m: mem.
+
+Inductive eval_annot_arg: annot_arg A -> val -> Prop :=
+  | eval_AA_base: forall x,
+      eval_annot_arg (AA_base x) (e x)
+  | eval_AA_int: forall n,
+      eval_annot_arg (AA_int n) (Vint n)
+  | eval_AA_long: forall n,
+      eval_annot_arg (AA_long n) (Vlong n)
+  | eval_AA_float: forall n,
+      eval_annot_arg (AA_float n) (Vfloat n)
+  | eval_AA_single: forall n,
+      eval_annot_arg (AA_single n) (Vsingle n)
+  | eval_AA_loadstack: forall chunk ofs v,
+      Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v ->
+      eval_annot_arg (AA_loadstack chunk ofs) v
+  | eval_AA_addrstack: forall ofs,
+      eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs))
+  | eval_AA_loadglobal: forall chunk id ofs v,
+      Mem.loadv chunk m (Senv.symbol_address ge id ofs) = Some v ->
+      eval_annot_arg (AA_loadglobal chunk id ofs) v
+  | eval_AA_addrglobal: forall id ofs,
+      eval_annot_arg (AA_addrglobal id ofs) (Senv.symbol_address ge id ofs)
+  | eval_AA_longofwords: forall hi lo vhi vlo,
+      eval_annot_arg hi vhi -> eval_annot_arg lo vlo ->
+      eval_annot_arg (AA_longofwords hi lo) (Val.longofwords vhi vlo).
+
+Definition eval_annot_args (al: list (annot_arg A)) (vl: list val) : Prop :=
+  list_forall2 eval_annot_arg al vl.
+
+Lemma eval_annot_arg_determ:
+  forall a v, eval_annot_arg a v -> forall v', eval_annot_arg a v' -> v' = v.
+Proof.
+  induction 1; intros v' EV; inv EV; try congruence.
+  f_equal; eauto.
+Qed.
+
+Lemma eval_annot_args_determ:
+  forall al vl, eval_annot_args al vl -> forall vl', eval_annot_args al vl' -> vl' = vl.
+Proof.
+  induction 1; intros v' EV; inv EV; f_equal; eauto using eval_annot_arg_determ.
+Qed.
+
+End EVAL_ANNOT_ARG.
+
+Hint Constructors eval_annot_arg: aarg.
+
+(** Invariance by change of global environment. *)
+
+Section EVAL_ANNOT_ARG_PRESERVED.
+
+Variables A F1 V1 F2 V2: Type.
+Variable ge1: Genv.t F1 V1.
+Variable ge2: Genv.t F2 V2.
+Variable e: A -> val.
+Variable sp: val.
+Variable m: mem.
+
+Hypothesis symbols_preserved:
+  forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id.
+
+Lemma eval_annot_arg_preserved:
+  forall a v, eval_annot_arg ge1 e sp m a v -> eval_annot_arg ge2 e sp m a v.
+Proof.
+  assert (EQ: forall id ofs, Senv.symbol_address ge2 id ofs = Senv.symbol_address ge1 id ofs).
+  { unfold Senv.symbol_address; simpl; intros. rewrite symbols_preserved; auto. }
+  induction 1; eauto with aarg. rewrite <- EQ in H; eauto with aarg. rewrite <- EQ; eauto with aarg. 
+Qed. 
 
+Lemma eval_annot_args_preserved:
+  forall al vl, eval_annot_args ge1 e sp m al vl -> eval_annot_args ge2 e sp m al vl.
+Proof.
+  induction 1; constructor; auto; eapply eval_annot_arg_preserved; eauto. 
+Qed.
 
+End EVAL_ANNOT_ARG_PRESERVED.
 
+(** Compatibility with the "is less defined than" relation. *)
 
+Section EVAL_ANNOT_ARG_LESSDEF.
 
+Variable A: Type.
+Variable ge: Senv.t.
+Variables e1 e2: A -> val.
+Variable sp: val.
+Variables m1 m2: mem.
+
+Hypothesis env_lessdef: forall x, Val.lessdef (e1 x) (e2 x).
+Hypothesis mem_extends: Mem.extends m1 m2.
+
+Lemma eval_annot_arg_lessdef:
+  forall a v1, eval_annot_arg ge e1 sp m1 a v1 ->
+  exists v2, eval_annot_arg ge e2 sp m2 a v2 /\ Val.lessdef v1 v2.
+Proof.
+  induction 1.
+- exists (e2 x); auto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. 
+- econstructor; eauto with aarg.
+- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg.
+- econstructor; eauto with aarg.
+- destruct IHeval_annot_arg1 as (vhi' & P & Q).
+  destruct IHeval_annot_arg2 as (vlo' & R & S).
+  econstructor; split; eauto with aarg. apply Val.longofwords_lessdef; auto. 
+Qed.
+
+Lemma eval_annot_args_lessdef:
+  forall al vl1, eval_annot_args ge e1 sp m1 al vl1 ->
+  exists vl2, eval_annot_args ge e2 sp m2 al vl2 /\ Val.lessdef_list vl1 vl2.
+Proof.
+  induction 1.
+- econstructor; split. constructor. auto.
+- exploit eval_annot_arg_lessdef; eauto. intros (v1' & P & Q). 
+  destruct IHlist_forall2 as (vl' & U & V).
+  exists (v1'::vl'); split; constructor; auto.
+Qed.
+
+End EVAL_ANNOT_ARG_LESSDEF.
 
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index c0eab04f..52aa963a 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -54,3 +54,28 @@ let name_of_external = function
   | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text)
   | EF_annot_val(text, targ) ->  sprintf "annot_val %S" (extern_atom text)
   | EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text)
+
+let rec print_annot_arg px oc = function
+  | AA_base x -> px oc x
+  | AA_int n -> fprintf oc "int %ld" (camlint_of_coqint n)
+  | AA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n)
+  | AA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n)
+  | AA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n)
+  | AA_loadstack(chunk, ofs) -> 
+      fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs)
+  | AA_addrstack(ofs) ->
+      fprintf oc "sp + %ld" (camlint_of_coqint ofs)
+  | AA_loadglobal(chunk, id, ofs) -> 
+      fprintf oc "%s[&%s + %ld]"
+              (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs)
+  | AA_addrglobal(id, ofs) ->
+      fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs)
+  | AA_longofwords(hi, lo) ->
+      fprintf oc "longofwords(%a, %a)" 
+                 (print_annot_arg px) hi (print_annot_arg px) lo
+
+let rec print_annot_args px oc = function
+  | [] -> ()
+  | [a] -> print_annot_arg px oc a
+  | a1 :: al ->
+      fprintf oc "%a, %a" (print_annot_arg px) a1 (print_annot_args px) al
diff --git a/common/Values.v b/common/Values.v
index a12fb636..12b380b7 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -111,15 +111,13 @@ Proof.
   simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto.
 Qed.
 
-(** Truth values.  Pointers and non-zero integers are treated as [True].
+(** Truth values.  Non-zero integers are treated as [True].
   The integer 0 (also used to represent the null pointer) is [False].
-  [Vundef] and floats are neither true nor false. *)
+  Other values are neither true nor false. *)
 
 Inductive bool_of_val: val -> bool -> Prop :=
   | bool_of_val_int:
-      forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero))
-  | bool_of_val_ptr:
-      forall b ofs, bool_of_val (Vptr b ofs) true.
+      forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero)).
 
 (** Arithmetic operations *)
 
@@ -695,7 +693,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
   | Vint n1, Vint n2 =>
       Some (Int.cmpu c n1 n2)
   | Vint n1, Vptr b2 ofs2 =>
-      if Int.eq n1 Int.zero then cmp_different_blocks c else None
+      if Int.eq n1 Int.zero && weak_valid_ptr b2 (Int.unsigned ofs2)
+      then cmp_different_blocks c
+      else None
   | Vptr b1 ofs1, Vptr b2 ofs2 =>
       if eq_block b1 b2 then
         if weak_valid_ptr b1 (Int.unsigned ofs1)
@@ -708,7 +708,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
         then cmp_different_blocks c
         else None
   | Vptr b1 ofs1, Vint n2 =>
-      if Int.eq n2 Int.zero then cmp_different_blocks c else None
+      if Int.eq n2 Int.zero && weak_valid_ptr b1 (Int.unsigned ofs1)
+      then cmp_different_blocks c
+      else None
   | _, _ => None
   end.
 
@@ -1175,8 +1177,8 @@ Proof.
   destruct c; auto. 
   destruct x; destruct y; simpl; auto.
   rewrite Int.negate_cmpu. auto.
-  destruct (Int.eq i Int.zero); auto. 
-  destruct (Int.eq i0 Int.zero); auto.
+  destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. 
+  destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto.
   destruct (eq_block b b0).
   destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) &&
             (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))).
@@ -1222,8 +1224,8 @@ Proof.
     destruct c; auto.
   destruct x; destruct y; simpl; auto.
   rewrite Int.swap_cmpu. auto.
-  case (Int.eq i Int.zero); auto.
-  case (Int.eq i0 Int.zero); auto.
+  destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto.
+  destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto.
   destruct (eq_block b b0); subst.
   rewrite dec_eq_true.
   destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1));
@@ -1381,6 +1383,12 @@ Proof.
   left; congruence. tauto. tauto.
 Qed.
 
+Lemma lessdef_list_trans:
+  forall vl1 vl2, lessdef_list vl1 vl2 -> forall vl3, lessdef_list vl2 vl3 -> lessdef_list vl1 vl3.
+Proof.
+  induction 1; intros vl3 LD; inv LD; constructor; eauto using lessdef_trans.
+Qed.
+
 (** Compatibility of operations with the [lessdef] relation. *)
 
 Lemma load_result_lessdef:
@@ -1423,19 +1431,23 @@ Lemma cmpu_bool_lessdef:
   cmpu_bool valid_ptr' c v1' v2' = Some b.
 Proof.
   intros. 
+  assert (A: forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true ->
+                           valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true).
+  { intros until ofs. rewrite ! orb_true_iff. intuition. }
   destruct v1; simpl in H2; try discriminate;
   destruct v2; simpl in H2; try discriminate;
   inv H0; inv H1; simpl; auto.
+  destruct (Int.eq i Int.zero && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))) eqn:E; try discriminate.
+  InvBooleans. rewrite H0, A by auto. auto. 
+  destruct (Int.eq i0 Int.zero && (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1))) eqn:E; try discriminate.
+  InvBooleans. rewrite H0, A by auto. auto. 
   destruct (eq_block b0 b1).
-  assert (forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true ->
-                        valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true).
-    intros until ofs. rewrite ! orb_true_iff. intuition. 
   destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)) eqn:?; try discriminate.
   destruct (valid_ptr b1 (Int.unsigned i0) || valid_ptr b1 (Int.unsigned i0 - 1)) eqn:?; try discriminate.
-  erewrite !H0 by eauto. auto.
+  erewrite ! A by eauto. auto.
   destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate.
   destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate.
-  erewrite !H by eauto. auto.
+  erewrite ! H by eauto. auto.
 Qed.
 
 Lemma of_optbool_lessdef:
@@ -1599,7 +1611,17 @@ Lemma val_cmpu_bool_inject:
 Proof.
   Local Opaque Int.add.
   intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-  fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
+- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+  destruct (Int.eq i Int.zero); auto.
+  destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate.
+  erewrite weak_valid_ptr_inj by eauto. auto. 
+- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
+  fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+  destruct (Int.eq i Int.zero); auto.
+  destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate.
+  erewrite weak_valid_ptr_inj by eauto. auto. 
+- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
   fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1.
   fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
   fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))).