Sketch for a formal version of PNVI-ae-udi.

theories/lang/pnvi.v

+From stdpp Require Export strings.
+From stdpp Require Import gmap list.
+From refinedc.lang Require Export base byte.
+Set Default Proof Using "Type".
+
+(* FIXME *)
+Section c_type.
+  Definition c_type := unit.
+
+  Definition size_of (τ : c_type) : N := 0%N.
+
+  Definition is_integer (τ : c_type) : bool := false.
+
+  Definition dearray (τ : c_type) : c_type := τ.
+End c_type.
+
+(** * Provenance *)
+
+Definition allocation_id := Z.
+
+Definition symbol := Z.
+
+Inductive provenance :=
+  (** No provenance. *)
+  | Pempty
+  (** Concrete provenance. *)
+  | Palloc_id (i : allocation_id)
+  (** Symbolic provenance. *)
+  | Psymbolic (ι : symbol).
+
+Notation "@empty" := (Pempty).
+Notation "@ i" := (@Palloc_id i) (at level 100).
+
+Instance provenance_eq_dec : EqDecision provenance.
+Proof.
+  move => p1 p2.
+  destruct p1 as [|i1|s1]; destruct p2 as [|i2|s2].
+  all: try by right.
+  - by left.
+  - destruct (decide (i1 = i2)) as [->|]; [by left | right => [][]//].
+  - destruct (decide (s1 = s2)) as [->|]; [by left | right => [][]//].
+Qed.
+
+(** * Memory state. *)
+
+(** Allocation map (A part). *)
+
+Definition address := N.
+
+Inductive kind := object | region.
+Inductive access := readWrite | readOnly.
+Inductive taint_flag := exposed | unexposed.
+
+Record allocation := Alloc {
+  (** Size of the allocation in bytes. *)
+  alloc_size : N;
+  (** Optional C type (None for regions, Some for objects). *)
+  alloc_type : option c_type;
+  (** Base address. *)
+  alloc_addr : address;
+  (** Is the allocation read-only? *)
+  alloc_access : access;
+  (** Allocation kind: it is an object? Otherwise region. *)
+  alloc_kind : kind;
+  (** Taint flag: has the allocaiton been exposed? *)
+  alloc_taint_flag : taint_flag;
+}.
+
+Definition expose_alloc (alloc : allocation) : allocation :=
+  match alloc with Alloc n τo a r k _ => Alloc n τo a r k exposed end.
+
+Inductive one_or_two_allocations :=
+  | One (a : allocation_id)
+  | Two (a1 a2 : allocation_id).
+
+Record allocation_map := AllocMap {
+  am_id_map : gmap allocation_id (option allocation); (* None is killed. *)
+  am_symb_map : gmap symbol one_or_two_allocations;
+}.
+
+Definition symb_set (A : allocation_map) (ι : symbol) : gset allocation_id :=
+  match A.(am_symb_map) !! ι with
+  | None             => ∅
+  | Some (One i)     => {[i]}
+  | Some (Two i1 i2) => {[i1; i2]}
+  end.
+
+(** Memory map (M part). *)
+
+Record abstract_byte := AByte {
+  abyte_prov : provenance;
+  abyte_byte : option byte; (* None is unspec. *)
+  abyte_index : option nat;
+}.
+
+Definition memory_map := gmap address abstract_byte.
+
+Fixpoint memory_write (m : memory_map) (a : address) bs :=
+  match bs with
+  | []      => m
+  | b :: bs => memory_write (<[a := b]> m) (N.succ a) bs
+  end.
+
+Fixpoint memory_read (m : memory_map) (a : address) (n : nat) :=
+  match n with
+  | O   => Some []
+  | S n => match memory_read m (N.succ a) n with
+           | None    => None
+           | Some bs => match m !! a with
+                        | None   => None
+                        | Some b => Some (b :: bs)
+                        end
+           end
+  end.
+
+(** State. *)
+
+Record mem_state := State {
+  state_alloc_map : allocation_map;
+  state_mem_map : memory_map;
+}.
+
+(** Pointer value. *)
+
+Inductive ptr_value :=
+  | Null
+  | Ptr (π : provenance) (a : address)
+  | FunPtr (id : string).
+
+Fixpoint go_combine_prov acc πs :=
+  match πs with
+  | []      => 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
+               end
+  end.
+
+(** * Value stuff. *)
+
+(* FIXME *)
+Section value.
+  Definition value := unit.
+
+  Definition repr (v : value) : list abstract_byte := [].
+
+  Definition abst (τ : value) (bs : list abstract_byte)
+                  : 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 :=
+  (a `mod` al = 0)%N ∧
+  a ≠ 0%N ∧
+  ∀ i alloc,
+    A.(am_id_map) !! i = Some (Some alloc) →
+    (alloc.(alloc_addr) + alloc.(alloc_size) ≤ a ∨
+     a + n ≤ alloc.(alloc_addr))%N.
+
+Inductive op := op_load | op_store.
+
+Definition bound_check op a n i A :=
+  ∃ alloc,
+    A.(am_id_map) !! i = Some (Some alloc) ∧
+    (alloc.(alloc_addr) ≤ a)%N ∧
+    (a + n - 1 ≤ alloc.(alloc_addr) + alloc.(alloc_size) - 1)%N ∧
+    match op with
+    | op_load  => True
+    | op_store => alloc.(alloc_access) = readWrite
+    end.
+
+Definition expose (A : allocation_map) (I : gset allocation_id) :=
+  let f i m :=
+    match m !! i with
+    | Some (Some alloc) => <[i := Some (expose_alloc alloc)]> m
+    | _                 => m
+    end
+  in
+  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 :=
+  | 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 →
+      let A' :=
+        let alloc := Some (Alloc n (Some τ) a readWrite object unexposed) in
+        AllocMap (<[i := alloc]> A.(am_id_map)) A.(am_symb_map)
+      in
+      mem_step
+        (State A M)
+        (allocate_object al τ None p)
+        (State A' M)
+  | Alloc_object_ro A M al τ p n a i v bs:
+      n = size_of τ →
+      A.(am_id_map) !! i = None →
+      valid_new_alloc a A al n →
+      p = Ptr (@i) a →
+      bs = repr v →
+      let A' :=
+        let alloc := Some (Alloc n (Some τ) a readOnly object unexposed) in
+        AllocMap (<[i := alloc]> A.(am_id_map)) A.(am_symb_map)
+      in
+      let M' := memory_write M a bs in
+      mem_step
+        (State A M)
+        (allocate_object al τ (Some v) p)
+        (State A' M')
+  | 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 →
+      let A' :=
+        let alloc := Some (Alloc n None a readWrite region unexposed) in
+        AllocMap (<[i := alloc]> A.(am_id_map)) A.(am_symb_map)
+      in
+      mem_step
+        (State A M)
+        (allocate_region al n p)
+        (State A' M)
+  | Kill A M k p i a alloc:
+      p = Ptr (@i) a →
+      A.(am_id_map) !! i = Some (Some alloc) →
+      a = alloc.(alloc_addr) →
+      k = alloc.(alloc_kind) →
+      let A' := AllocMap (<[i := None]> A.(am_id_map)) A.(am_symb_map) in
+      mem_step
+        (State A M)
+        (kill k p)
+        (State A' M)
+  | Kill_null A M p:
+      p = Null →
+      mem_step
+        (State A M)
+        (kill region p)
+        (State A M)
+  | Kill_iota A M k p ι a ids i:
+      p = Ptr (Psymbolic ι) a →
+      A.(am_symb_map) !! ι = Some ids →
+      (match ids with
+       | One j     =>
+         ∃ alloc,
+           A.(am_id_map) !! j = Some (Some alloc) ∧
+           i = j ∧
+           alloc.(alloc_addr) = a ∧
+           alloc.(alloc_kind) = k
+       | Two j1 j2 =>
+         ∃ alloc1 alloc2,
+           A.(am_id_map) !! j1 = Some (Some alloc1) ∧
+           A.(am_id_map) !! j2 = Some (Some alloc2) ∧
+           j1 ≠ j2 ∧
+           (i = j1 ∧ alloc1.(alloc_addr) = a ∧ alloc1.(alloc_kind) = k) ∨
+           (i = j2 ∧ alloc2.(alloc_addr) = a ∧ alloc2.(alloc_kind) = k)
+       end) →
+      let A' :=
+        AllocMap
+          (<[i := None]> A.(am_id_map))
+          (<[ι := One i]> A.(am_symb_map))
+      in
+      mem_step
+        (State A M)
+        (kill k p)
+        (State A' M)
+  | Load A M τ p v a i n bs I_tainted:
+      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 →
+      abst τ bs = Some (v, I_tainted) →
+      let A' := if is_integer τ then expose A I_tainted else A in
+      mem_step
+        (State A M)
+        (load τ p v)
+        (State A' M)
+  | Load_iota A M τ p v a ι n ids i bs I_tainted:
+      p = Ptr (Psymbolic ι) a →
+      n = size_of τ →
+      bound_check op_load a n i A →
+      A.(am_symb_map) !! ι = Some ids →
+      match ids with One j => i = j | Two j1 j2 => i = j1 ∨ i = j2 end →
+      memory_read M a (N.to_nat n) = Some bs →
+      abst τ bs = Some (v, I_tainted) →
+      let A' := if is_integer τ then expose A I_tainted else A in
+      let A'' := AllocMap A'.(am_id_map) (<[ι := One i]> A'.(am_symb_map)) in
+      mem_step
+        (State A M)
+        (load τ p v)
+        (State A'' M)
+  | Store A M τ p v i a n:
+      p = Ptr (@i) a →
+      n = size_of τ →
+      bound_check op_store a n i A →
+      let M' := memory_write M a (repr v) in
+      mem_step
+        (State A M)
+        (store τ p v)
+        (State A M')
+  | Store_iota A M τ p v ι a n ids i:
+      p = Ptr (Psymbolic ι) a →
+      n = size_of τ →
+      bound_check op_store a n i A →
+      A.(am_symb_map) !! ι = Some ids →
+      match ids with One j => i = j | Two j1 j2 => i = j1 ∨ i = j2 end →
+      let A' := AllocMap A.(am_id_map) (<[ι := One i]> A.(am_symb_map)) in
+      let M' := memory_write M a (repr v) in
+      mem_step
+        (State A M)
+        (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 →
+      i1 = i2 →
+      A.(am_id_map) !! i1 = Some (Some alloc) →
+      (alloc.(alloc_addr) ≤ a1 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
+      (alloc.(alloc_addr) ≤ a2 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
+      x = (Z.of_N a1 - Z.of_N a2) / Z.of_N (size_of (dearray τ)) →
+      mem_step
+        (State A M)
+        (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 →
+      p2 = Ptr (Psymbolic ι) a2 →
+      i ∈ symb_set A ι →
+      A.(am_id_map) !! i = Some (Some alloc) →
+      (alloc.(alloc_addr) ≤ a1 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
+      (alloc.(alloc_addr) ≤ a2 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
+      x = (Z.of_N a1 - Z.of_N a2) / Z.of_N (size_of (dearray τ)) →
+      let A' := AllocMap A.(am_id_map) (<[ι := One i]> A.(am_symb_map)) in
+      mem_step
+        (State A M)
+        (diff_ptrval τ p1 p2 x)
+        (State A' M)
+  | Diff_ptrval_iota_l A M τ p1 p2 x ι a1 i a2 alloc:
+      p1 = Ptr (Psymbolic ι) 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 →
+      (alloc.(alloc_addr) ≤ a2 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
+      x = (Z.of_N a1 - Z.of_N a2) / Z.of_N (size_of (dearray τ)) →
+      let A' := AllocMap A.(am_id_map) (<[ι := One i]> A.(am_symb_map)) in
+      mem_step
+        (State A M)
+        (diff_ptrval τ p1 p2 x)
+        (State A' M)
+  | Diff_ptrval_iota_both A M τ p1 p2 x ι1 a1 ι2 a2 i1 i2 alloc1 alloc2:
+      p1 = Ptr (Psymbolic ι1) a2 →
+      p2 = Ptr (Psymbolic ι2) a2 →
+      symb_set A ι1 = {[i1; i2]} →
+      symb_set A ι2 = {[i1; i2]} →
+      A.(am_id_map) !! i1 = Some (Some alloc1) →
+      A.(am_id_map) !! i2 = Some (Some alloc2) →
+      (alloc1.(alloc_addr) ≤ a1 ≤ alloc1.(alloc_addr) + alloc1.(alloc_size))%N →
+      (alloc1.(alloc_addr) ≤ a2 ≤ alloc1.(alloc_addr) + alloc1.(alloc_size))%N →
+      (alloc2.(alloc_addr) ≤ a1 ≤ alloc2.(alloc_addr) + alloc2.(alloc_size))%N →
+      (alloc2.(alloc_addr) ≤ a2 ≤ alloc2.(alloc_addr) + alloc2.(alloc_size))%N →
+      x = 0 →
+      mem_step
+        (State A M)
+        (diff_ptrval τ p1 p2 x)
+        (State A M)
+  | Diff_ptrval_iota_inter A M τ p1 p2 x ι1 a1 ι2 a2 i alloc:
+      p1 = Ptr (Psymbolic ι1) a2 →
+      p2 = Ptr (Psymbolic ι2) a2 →
+      symb_set A ι1 ∩ symb_set A ι2 = {[i]} →
+      A.(am_id_map) !! i = Some (Some alloc) →
+      (alloc.(alloc_addr) ≤ a1 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
+      (alloc.(alloc_addr) ≤ a2 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
+      x = (Z.of_N a1 - Z.of_N a2) / Z.of_N (size_of (dearray τ)) →
+      let A' :=
+        AllocMap A.(am_id_map) (<[ι1 := One i]> (<[ι2 := One i]> A.(am_symb_map)))
+      in
+      mem_step
+        (State A M)
+        (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 →
+      i1 = i2 →
+      A.(am_id_map) !! i1 = Some (Some alloc) →
+      (alloc.(alloc_addr) ≤ a1 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
+      (alloc.(alloc_addr) ≤ a2 ≤ alloc.(alloc_addr) + alloc.(alloc_size))%N →
+      b = interp_rel_op op a1 a2 →
+      mem_step
+        (State A M)
+        (relop_ptrval op p1 p2 b)
+        (State A M)
+  | Pointer_equality A M p1 p2 b:
+      (* TODO which version? *)
+      mem_step
+        (State A M)
+        (eq_ptrval p1 p2 b)
+        (State A M)
+  (* TODO pointer array offset. Which version? *)
+  (* TODO pointer struct/union member offset. Which version? *)
+  | Intptr_cast_null A M τ x p:
+      x = 0 →
+      p = Null →
+      mem_step
+        (State A M)
+        (cast_ival_to_ptrval τ x p)
+        (State A M)
+  | Intptr_cast A M τ x p i a alloc:
+      A.(am_id_map) !! i = Some (Some alloc) →
+      (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 →
+      mem_step
+        (State A M)
+        (cast_ival_to_ptrval τ x p )
+        (State A M)
+  | Intptr_cast_iota A M τ x p i1 i2 a alloc1 alloc2 ι:
+      i1 ≠ i2 →
+      A.(am_id_map) !! i1 = Some (Some alloc1) →
+      A.(am_id_map) !! i2 = Some (Some alloc2) →
+      (alloc1.(alloc_addr) ≤ a ≤ alloc1.(alloc_addr) + alloc1.(alloc_size))%N →
+      alloc1.(alloc_taint_flag) = exposed →
+      (alloc2.(alloc_addr) ≤ a ≤ alloc2.(alloc_addr) + alloc2.(alloc_size))%N →
+      alloc2.(alloc_taint_flag) = exposed →
+      A.(am_symb_map) !! ι = None →
+      p = Ptr (Psymbolic ι) a →
+      let A' := AllocMap A.(am_id_map) (<[ι := Two i1 i2]> A.(am_symb_map)) in
+      mem_step
+        (State A M)
+        (cast_ival_to_ptrval τ x p)
+        (State A' M)
+  | Intptr_cast_fallback A M τ x p a:
+      (* FIXME check no candidate alloc? *)
+      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. *)
+      A.(am_id_map) !! i = Some (Some alloc) →
+      x = Z.of_N a →
+      let A' := expose A {[i]} in
+      mem_step
+        (State A M)
+        (cast_ptrval_to_ival τ p x)
+        (State A' M)
+.