From a635aff1bcf9ff700a136d6b15560633838f1f3c Mon Sep 17 00:00:00 2001
From: Scott Owens <sowens@fb.com>
Date: Wed, 14 Aug 2019 06:58:12 -0700
Subject: [PATCH] Finish proving sanity checking property

Summary:
There could very well still be bugs in the semantics, since the
invariant here doesn't say all that much, and it completely ignores
local registers. But most trivial things and typos are probably fixed.

Reviewed By: jberdine

Differential Revision: D16803281

fbshipit-source-id: 48ba2523b
---
 sledge/semantics/llvmScript.sml      | 125 ++++++++++++++++-----------
 sledge/semantics/llvm_propScript.sml |  57 ++++++++++--
 2 files changed, 124 insertions(+), 58 deletions(-)

diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 48006eed2..d62276197 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -152,10 +152,12 @@ Datatype `
        (* The set of allocated ranges. The bool indicates whether the range is
         * free-able or not *)
        allocations : (bool # num # num) set;
+       (* A byte addressed heap, with a poison tag *)
        heap : addr |-> bool # word8 |>`;
 
 (* ----- Things about types ----- *)
 
+(* How many bytes a value of the given type occupies *)
 Definition sizeof_def:
   (sizeof (IntT W1) = 1) ∧
   (sizeof (IntT W8) = 1) ∧
@@ -232,6 +234,7 @@ Definition bool_to_v_def:
   bool_to_v b = if b then W1V 1w else W1V 0w
 End
 
+(* Calculate the offset given by a list of indices *)
 Definition get_offset_def:
   (get_offset _ [] = Some 0) ∧
   (get_offset (ArrT _ t) (i::is) =
@@ -294,14 +297,6 @@ Definition v2n_def:
   (v2n _ = None)
 End
 
-Definition update_result_def:
-  update_result x v s = s with locals := s.locals |+ (x, v)
-End
-
-Definition inc_pc_def:
-  inc_pc s = s with ip := (s.ip with i := s.ip.i + 1)
-End
-
 Definition interval_to_set_def:
   interval_to_set (_, start,stop) =
     { n | start ≤ n ∧ n < stop }
@@ -324,6 +319,16 @@ Definition is_free_def:
     ∀b2. b2 ∈ allocs ⇒ interval_to_set b1 ∩ interval_to_set b2 = ∅
 End
 
+Definition get_bytes_def:
+  get_bytes h (_, start, stop) =
+    map
+      (λoff.
+        case flookup h (A (start + off)) of
+        | None => (F, 0w)
+        | Some w => w)
+      (count_list (stop - start))
+End
+
 Definition set_bytes_def:
   (set_bytes p [] n h = h) ∧
   (set_bytes p (b::bs) n h =
@@ -349,16 +354,8 @@ Definition deallocate_def:
       (allocs DIFF to_remove, fdiff h (image A (bigunion (image interval_to_set to_remove))))
 End
 
-Definition get_bytes_def:
-  get_bytes h (_, start, stop) =
-    map
-      (λoff.
-        case flookup h (A (start + off)) of
-        | None => (F, 0w)
-        | Some w => w)
-      (count_list (stop - start))
-End
-
+(* Read len bytes from the list of bytes, and convert it into a word value,
+ * little-endian encoding *)
 Definition le_read_w_def:
   le_read_w len (bs : word8 list) =
     if length bs < len then
@@ -367,6 +364,7 @@ Definition le_read_w_def:
       (l2w 256 (map w2n (take len bs)), drop len bs)
 End
 
+(* Return len bytes that are the little-endian encoding of the argument word *)
 Definition le_write_w_def:
   le_write_w len w =
     let (l : word8 list) = map n2w (w2l 256 w) in
@@ -470,6 +468,14 @@ Definition insert_value_def:
   (insert_value _ _ _ = None)
 End
 
+Definition update_result_def:
+  update_result x v s = s with locals := s.locals |+ (x, v)
+End
+
+Definition inc_pc_def:
+  inc_pc s = s with ip := (s.ip with i := s.ip.i + 1)
+End
+
 (* NB, the semantics tracks the poison values, but not much thought has been put
  * into getting it exactly right, so we don't have much confidence that it is
  * exactly right. We also are currently ignoring the undefined value. *)
@@ -601,12 +607,14 @@ Inductive step_instr:
      (Call r t fname targs)
      <| ip := <| f := fname; b := None; i := 0 |>;
         locals := alist_to_fmap (zip (d.params, map (eval s o snd) targs));
+        globals := s.globals;
+        allocations:= s.allocations;
         stack :=
           <| ret := s.ip with i := s.ip.i + 1;
              saved_locals := s.locals;
              result_var := r;
              stack_allocs := [] |> :: s.stack;
-        heap := heap |>) ∧
+        heap := s.heap |>) ∧
 
   (* TODO *)
   (step_instr prog s (Cxa_allocate_exn r a) s) ∧
@@ -635,8 +643,9 @@ Inductive step:
   step p s s'
 End
 
-(* ----- Initial state ----- *)
+(* ----- Invariants on state ----- *)
 
+(* The allocations are of intervals that don't overlap *)
 Definition allocations_ok_def:
   allocations_ok s ⇔
     ∀i1 i2.
@@ -646,11 +655,13 @@ Definition allocations_ok_def:
       (interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒ i1 = i2)
 End
 
+(* The heap maps exactly the address in the allocations *)
 Definition heap_ok_def:
   heap_ok s ⇔
     ∀n. flookup s.heap (A n) ≠ None ⇔ ∃i. i ∈ s.allocations ∧ n ∈ interval_to_set i
 End
 
+(* All global variables are allocated in non-freeable memory *)
 Definition globals_ok_def:
   globals_ok s ⇔
     ∀g n w.
@@ -659,47 +670,36 @@ Definition globals_ok_def:
       is_allocated (F, w2n w, w2n w + n) s.allocations
 End
 
-(* The initial state contains allocations for the initialised global variables *)
-Definition is_init_state_def:
-  is_init_state s (global_init : glob_var |-> ty # v) ⇔
-    s.ip.f = Fn "main" ∧
-    s.ip.b = None ∧
-    s.ip.i = 0 ∧
-    s.locals = fempty ∧
-    s.stack = [] ∧
-    allocations_ok s ∧
-    globals_ok s ∧
-    fdom s.globals = fdom global_init ∧
-    s.allocations ⊆ {F, start, stop | T} ∧
-    ∀g w t v n.
-      flookup s.globals g = Some (n, w) ∧ flookup global_init g = Some (t,v) ⇒
-      ∃bytes.
-        get_bytes s.heap (F, w2n w, w2n w + sizeof t) = map (λb. (F,b)) bytes ∧
-        bytes_to_value t bytes = (v, [])
-End
-
-(* ----- Invariants on state ----- *)
-
-Definition prog_ok_def:
-  prog_ok p ⇔
-    ∀fname dec bname block.
-      flookup p fname = Some dec ∧
-      flookup dec.blocks bname = Some block
-      ⇒
-      block.body ≠ [] ∧ terminator (last block.body)
-End
-
+(* Instruction pointer points to an instruction *)
 Definition ip_ok_def:
   ip_ok p ip ⇔
     ∃dec block. flookup p ip.f = Some dec ∧ flookup dec.blocks ip.b = Some block ∧ ip.i < length block.body
 End
 
+Definition prog_ok_def:
+  prog_ok p ⇔
+    ((* All blocks end with terminators *)
+     ∀fname dec bname block.
+       flookup p fname = Some dec ∧
+       flookup dec.blocks bname = Some block
+       ⇒
+       block.body ≠ [] ∧ terminator (last block.body)) ∧
+    ((* All functions have an entry block *)
+     ∀fname dec.
+       flookup p fname = Some dec ⇒ ∃block. flookup dec.blocks None = Some block) ∧
+     (* There is a main function *)
+     ∃dec. flookup p (Fn "main") = Some dec
+End
+
+(* All call frames have a good return address, and the stack allocations of the
+ * frame are all in freeable memory *)
 Definition frame_ok_def:
   frame_ok p s f ⇔
     ip_ok p f.ret ∧
     every (λn. ∃start stop. n = A start ∧ (T, start, stop) ∈ s.allocations) f.stack_allocs
 End
 
+(* The frames are all of, and no two stack allocations have the same address *)
 Definition stack_ok_def:
   stack_ok p s ⇔
     every (frame_ok p s) s.stack ∧
@@ -711,4 +711,29 @@ Definition state_invariant_def:
     ip_ok p s.ip ∧ allocations_ok s ∧ heap_ok s ∧ globals_ok s ∧ stack_ok p s
 End
 
+(* ----- Initial state ----- *)
+
+(* The initial state contains allocations for the initialised global variables *)
+Definition is_init_state_def:
+  is_init_state s (global_init : glob_var |-> ty # v) ⇔
+    s.ip.f = Fn "main" ∧
+    s.ip.b = None ∧
+    s.ip.i = 0 ∧
+    s.locals = fempty ∧
+    s.stack = [] ∧
+    allocations_ok s ∧
+    globals_ok s ∧
+    heap_ok s ∧
+    fdom s.globals = fdom global_init ∧
+    (* The initial allocations for globals are not freeable *)
+    s.allocations ⊆ { (F, start, stop) | T } ∧
+    (* The heap starts with the initial values of the globals written to their
+     * addresses *)
+    ∀g w t v n.
+      flookup s.globals g = Some (n, w) ∧ flookup global_init g = Some (t,v) ⇒
+      ∃bytes.
+        get_bytes s.heap (F, w2n w, w2n w + sizeof t) = map (λb. (F,b)) bytes ∧
+        bytes_to_value t bytes = (v, [])
+End
+
 export_theory();
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index 3c58d1b2e..20b8db6c6 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -686,7 +686,7 @@ Theorem step_instr_invariant:
     state_invariant p s2
 Proof
   ho_match_mp_tac step_instr_ind >> rw []
-  >- (
+  >- ( (* Ret *)
     rw [update_invariant] >> fs [state_invariant_def] >> rw []
     >- (
       fs [stack_ok_def] >> rfs [EVERY_EL, frame_ok_def] >>
@@ -711,8 +711,26 @@ Proof
         metis_tac [])
       >- (
         fs [ALL_DISTINCT_APPEND])))
-  >- cheat
-  >- cheat
+  >- ( (* Br *)
+    fs [state_invariant_def] >> rw []
+    >- (
+      rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
+      qpat_x_assum `flookup _ (Fn "main") = _` kall_tac >>
+      last_x_assum drule >> disch_then drule >> fs [])
+    >- (fs [allocations_ok_def] >> metis_tac [])
+    >- (fs [heap_ok_def] >> metis_tac [])
+    >- (fs [globals_ok_def] >> metis_tac [])
+    >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
+  >- ( (* Br *)
+    fs [state_invariant_def] >> rw []
+    >- (
+      rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
+      qpat_x_assum `flookup _ (Fn "main") = _` kall_tac >>
+      last_x_assum drule >> disch_then drule >> fs [])
+    >- (fs [allocations_ok_def] >> metis_tac [])
+    >- (fs [heap_ok_def] >> metis_tac [])
+    >- (fs [globals_ok_def] >> metis_tac [])
+    >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]>>
     metis_tac [terminator_def])
@@ -722,8 +740,7 @@ Proof
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
     metis_tac [terminator_def])
-  >- (
-    (* Allocation *)
+  >- ( (* Allocation *)
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
     >- metis_tac [allocate_invariant]
     >- (fs [next_instr_cases, allocate_cases] >> metis_tac [terminator_def]))
@@ -731,8 +748,7 @@ Proof
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
     fs [next_instr_cases] >>
     metis_tac [terminator_def])
-  >- (
-    (* Store *)
+  >- ( (* Store *)
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
     >- (irule set_bytes_invariant >> rw [] >> metis_tac [])
     >- (fs [next_instr_cases] >> metis_tac [terminator_def]))
@@ -748,7 +764,32 @@ Proof
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
     metis_tac [terminator_def])
-  >- cheat
+  >- ( (* Call *)
+    rw [state_invariant_def]
+    >- (fs [prog_ok_def, ip_ok_def] >> metis_tac [NOT_NIL_EQ_LENGTH_NOT_0])
+    >- (fs [state_invariant_def, allocations_ok_def] >> metis_tac [])
+    >- (fs [state_invariant_def, heap_ok_def] >> metis_tac [])
+    >- (fs [state_invariant_def, globals_ok_def] >> metis_tac [])
+    >- (
+      fs [state_invariant_def, stack_ok_def] >> rw []
+      >- (
+        rw [frame_ok_def] >> fs [ip_ok_def, prog_ok_def] >>
+        last_x_assum drule >> disch_then drule >> rw [] >>
+        CCONTR_TAC >> fs [] >> rfs [LAST_EL] >>
+        Cases_on `length block'.body = s1.ip.i + 1` >> fs [PRE_SUB1] >>
+        fs [next_instr_cases] >>
+        metis_tac [terminator_def])
+      >- (fs [EVERY_MEM, frame_ok_def] >> metis_tac [])))
+QED
+
+(* ----- Initial state is ok ----- *)
+
+Theorem init_invariant:
+  ∀p s init. prog_ok p ∧ is_init_state s init ⇒ state_invariant p s
+Proof
+  rw [is_init_state_def, state_invariant_def]
+  >- (rw [ip_ok_def] >> fs [prog_ok_def] >> metis_tac [NOT_NIL_EQ_LENGTH_NOT_0])
+  >- rw [stack_ok_def]
 QED
 
 export_theory ();