Abstract away the events.

theories/lang/pnvi.v

@@ -14,6 +14,49 @@ Section c_type.
   Definition dearray (τ : c_type) : c_type := τ.
 End c_type.
 
+Definition tag_symb := string. (* FIXME *)
+Definition memb_ident := string.
+
+(** Allocation kind. *)
+Inductive allocation_kind := object | region.
+
+(** Relational operator. *)
+Inductive rel_op := Lt | Le | Gt | Ge.
+
+(** Generic notion of event. *)
+Section event.
+  Context {ptr_value int_value value : Set}.
+
+  Inductive event :=
+    (** allocate_object(al, τ, {readWrite|readOnly(v)}) = p *)
+    | allocate_object (al : N) (τ : c_type) (v : option value) (p : ptr_value)
+    (** allocate_region(al, n) = p *)
+    | allocate_region (al : N) (n : N) (p : ptr_value)
+    (** kill_{object|region}(p) *)
+    | kill (k : allocation_kind) (p : ptr_value)
+    (** load(τ, p) = v *)
+    | load (τ : c_type) (p : ptr_value) (v : value) (* FIXME add footprint? *)
+    (** store(τ, p, v) *)
+    | store (τ : c_type) (p : ptr_value) (v : value) (* FIXME add footprint? *)
+    (** diff_ptrval(τ, p1, p2) = x *)
+    | diff_ptrval (τ : c_type) (p1 p2 : ptr_value) (x : int_value)
+    (** relop_ptrval(op, p1, p2) = b *)
+    | relop_ptrval (op : rel_op) (p1 p2 : ptr_value) (b : bool)
+    (** eq_ptrval(p1, p2) = b *)
+    | eq_ptrval (p1 p2 : ptr_value) (b : bool)
+    (** array_offset(p, τ, n) = p' *)
+    | array_offset (p : ptr_value) (τ : c_type) (n : N) (p' : ptr_value)
+    (** member_offset(p, T, x) = p' *)
+    | member_offset (p : ptr_value) (T : tag_symb) (x : memb_ident) (p' : ptr_value)
+    (** cast_ival_to_ptrval(τ, x) = p *)
+    | cast_ival_to_ptrval (τ : c_type) (x : int_value) (p : ptr_value)
+    (** cast_ptrval_to_ival(τ, p) = x *)
+    | cast_ptrval_to_ival (τ : c_type) (p : ptr_value) (x : int_value)
+    (** copy_alloc_id(τ, x, p) = p' - only used by Caesium. *)
+    | copy_alloc_id (τ : c_type) (x : int_value) (p : ptr_value) (p' : ptr_value)
+  .
+End event.
+
 (** * Provenance *)
 
 Definition allocation_id := Z.
@@ -28,8 +71,8 @@ Inductive provenance :=
   (** Symbolic provenance. *)
   | Psymbolic (ι : symbol).
 
-Notation "@empty" := (Pempty).
-Notation "@ i" := (@Palloc_id i) (at level 100).
+Notation "$empty" := (Pempty).
+Notation "$ i" := (Palloc_id i) (at level 10).
 
 Instance provenance_eq_dec : EqDecision provenance.
 Proof.
@@ -47,7 +90,6 @@ Qed.
 
 Definition address := N.
 
-Inductive kind := object | region.
 Inductive access := readWrite | readOnly.
 Inductive taint_flag := exposed | unexposed.
 
@@ -61,7 +103,7 @@ Record allocation := Alloc {
   (** Is the allocation read-only? *)
   alloc_access : access;
   (** Allocation kind: it is an object? Otherwise region. *)
-  alloc_kind : kind;
+  alloc_kind : allocation_kind;
   (** Taint flag: has the allocaiton been exposed? *)
   alloc_taint_flag : taint_flag;
 }.
@@ -129,13 +171,13 @@ Inductive ptr_value :=
 
 Fixpoint go_combine_prov acc πs :=
   match πs with
-  | []      => default @empty acc
+  | []      => default $empty acc
   | π :: πs => match acc with
                | None    => go_combine_prov (Some π) πs
                | Some π' => if bool_decide (π = π') then
                               go_combine_prov acc πs
                             else
-                              @empty
+                              $empty
                end
   end.
 
@@ -151,45 +193,6 @@ Section value.
                   : option (value * gset allocation_id) := Some ((), ∅).
 End value.
 
-(** * Events. *)
-
-Inductive rel_op := Lt | Le | Gt | Ge.
-
-Definition interp_rel_op (op : rel_op) (a1 a2 : address) : bool :=
-  match op with
-  | Lt => bool_decide (a1 < a2)%N
-  | Le => bool_decide (a1 ≤ a2)%N
-  | Gt => bool_decide (¬ (a1 ≤ a2))%N
-  | Ge => bool_decide (¬ (a1 < a2))%N
-  end.
-
-Inductive event :=
-  (** allocate_object(al, τ, {readWrite|readOnly(v)}) = p *)
-  | allocate_object (al : N) (τ : c_type) (v : option value) (p : ptr_value)
-  (** allocate_region(al, n) = p *)
-  | allocate_region (al : N) (n : N) (p : ptr_value)
-  (** kill_{object|region}(p) *)
-  | kill (kind : kind) (p : ptr_value)
-  (** load(τ, p) = v *)
-  | load (τ : c_type) (p : ptr_value) (v : value) (* FIXME add footprint? *)
-  (** store(τ, p, v) *)
-  | store (τ : c_type) (p : ptr_value) (v : value) (* FIXME add footprint? *)
-  (** diff_ptrval(τ, p1, p2) = x *)
-  | diff_ptrval (τ : c_type) (p1 p2 : ptr_value) (x : Z)
-  (** relop_ptrval(op, p1, p2) = b *)
-  | relop_ptrval (op : rel_op) (p1 p2 : ptr_value) (b : bool)
-  (** eq_ptrval(p1, p2) = b *)
-  | eq_ptrval (p1 p2 : ptr_value) (b : bool)
-  (** array_offset(p, τ, n) = p' *)
-  | array_offset (p : ptr_value) (τ : c_type) (n : N) (p' : ptr_value)
-  (** member_offset(p, T, x) = p' *)
-  | member_offset (p : ptr_value) (T : unit) (x : unit) (p' : ptr_value) (* FIXME *)
-  (** cast_ival_to_ptrval(τ, x) = p *)
-  | cast_ival_to_ptrval (τ : c_type) (x : Z) (p : ptr_value)
-  (** cast_ptrval_to_ival(τ, p) = x *)
-  | cast_ptrval_to_ival (τ : c_type) (p : ptr_value) (x : Z)
-.
-
 (** Allocating an object or a region. *)
 
 Definition valid_new_alloc a (A : allocation_map) al n :=
@@ -222,12 +225,22 @@ Definition expose (A : allocation_map) (I : gset allocation_id) :=
   let m := set_fold f A.(am_id_map) I in
   AllocMap m A.(am_symb_map).
 
-Inductive mem_step : mem_state → event → mem_state → Prop :=
+Definition interp_rel_op (op : rel_op) (a1 a2 : address) : bool :=
+  match op with
+  | Lt => bool_decide (a1 < a2)%N
+  | Le => bool_decide (a1 ≤ a2)%N
+  | Gt => bool_decide (¬ (a1 ≤ a2))%N
+  | Ge => bool_decide (¬ (a1 < a2))%N
+  end.
+
+Definition PNVI_event := @event ptr_value Z value.
+
+Inductive mem_step : mem_state → PNVI_event → mem_state → Prop :=
   | Alloc_object_rw A M al τ p n a i:
       n = size_of τ →
       A.(am_id_map) !! i = None →
       valid_new_alloc a A al n →
-      p = Ptr (@i) a →
+      p = Ptr ($ i) a →
       let A' :=
         let alloc := Some (Alloc n (Some τ) a readWrite object unexposed) in
         AllocMap (<[i := alloc]> A.(am_id_map)) A.(am_symb_map)
@@ -240,7 +253,7 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
       n = size_of τ →
       A.(am_id_map) !! i = None →
       valid_new_alloc a A al n →
-      p = Ptr (@i) a →
+      p = Ptr ($i) a →
       bs = repr v →
       let A' :=
         let alloc := Some (Alloc n (Some τ) a readOnly object unexposed) in
@@ -254,7 +267,7 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
   | Alloc_region A M al p n a i:
       A.(am_id_map) !! i = None →
       valid_new_alloc a A al n →
-      p = Ptr (@i) a →
+      p = Ptr ($i) a →
       let A' :=
         let alloc := Some (Alloc n None a readWrite region unexposed) in
         AllocMap (<[i := alloc]> A.(am_id_map)) A.(am_symb_map)
@@ -264,7 +277,7 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
         (allocate_region al n p)
         (State A' M)
   | Kill A M k p i a alloc:
-      p = Ptr (@i) a →
+      p = Ptr ($i) a →
       A.(am_id_map) !! i = Some (Some alloc) →
       a = alloc.(alloc_addr) →
       k = alloc.(alloc_kind) →
@@ -307,7 +320,7 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
         (kill k p)
         (State A' M)
   | Load A M τ p v a i n bs I_tainted:
-      p = Ptr (@i) a →
+      p = Ptr ($i) a →
       n = size_of τ →
       bound_check op_load a n i A →
       memory_read M a (N.to_nat n) = Some bs →
@@ -332,7 +345,7 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
         (load τ p v)
         (State A'' M)
   | Store A M τ p v i a n:
-      p = Ptr (@i) a →
+      p = Ptr ($i) a →
       n = size_of τ →
       bound_check op_store a n i A →
       let M' := memory_write M a (repr v) in
@@ -353,8 +366,8 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
         (store τ p v)
         (State A' M')
   | Diff_ptrval A M τ p1 p2 x i1 a1 i2 a2 alloc:
-      p1 = Ptr (@i1) a1 →
-      p2 = Ptr (@i2) a2 →
+      p1 = Ptr ($i1) a1 →
+      p2 = Ptr ($i2) a2 →
       i1 = i2 →
       A.(am_id_map) !! i1 = Some (Some alloc) →
       (alloc.(alloc_addr) ≤ a1 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
@@ -365,7 +378,7 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
         (diff_ptrval τ p1 p2 x)
         (State A M)
   | Diff_ptrval_iota_r A M τ p1 p2 x i a1 ι a2 alloc:
-      p1 = Ptr (@i) a1 →
+      p1 = Ptr ($i) a1 →
       p2 = Ptr (Psymbolic ι) a2 →
       i ∈ symb_set A ι →
       A.(am_id_map) !! i = Some (Some alloc) →
@@ -379,7 +392,7 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
         (State A' M)
   | Diff_ptrval_iota_l A M τ p1 p2 x ι a1 i a2 alloc:
       p1 = Ptr (Psymbolic ι) a2 →
-      p2 = Ptr (@i) a2 →
+      p2 = Ptr ($i) a2 →
       i ∈ symb_set A ι →
       A.(am_id_map) !! i = Some (Some alloc) →
       (alloc.(alloc_addr) ≤ a1 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
@@ -422,8 +435,8 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
         (diff_ptrval τ p1 p2 x)
         (State A' M)
   | Pointer_relop A M op p1 p2 b i1 a1 i2 a2 alloc:
-      p1 = Ptr (@i1) a1 →
-      p2 = Ptr (@i2) a2 →
+      p1 = Ptr ($i1) a1 →
+      p2 = Ptr ($i2) a2 →
       i1 = i2 →
       A.(am_id_map) !! i1 = Some (Some alloc) →
       (alloc.(alloc_addr) ≤ a1 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
@@ -453,7 +466,7 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
       (alloc.(alloc_addr) ≤ a ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
       alloc.(alloc_taint_flag) = exposed →
       (* FIXME ensure no other candidate alloc? *)
-      p = Ptr (@i) a →
+      p = Ptr ($i) a →
       mem_step
         (State A M)
         (cast_ival_to_ptrval τ x p )
@@ -475,13 +488,13 @@ Inductive mem_step : mem_state → event → mem_state → Prop :=
         (State A' M)
   | Intptr_cast_fallback A M τ x p a:
       (* FIXME check no candidate alloc? *)
-      p = Ptr (@empty) a →
+      p = Ptr ($empty) a →
       mem_step
         (State A M)
         (cast_ival_to_ptrval τ x p)
         (State A M)
   | Ptrint_cast A M τ p x i a alloc:
-      p = Ptr (@i) a → (* FIXME What about other shapes of pointers. *)
+      p = Ptr ($i) a → (* FIXME What about other shapes of pointers. *)
       A.(am_id_map) !! i = Some (Some alloc) →
       x = Z.of_N a →
       let A' := expose A {[i]} in