From d864fb2c89a6f3b6a4b5cb0c86591f2fb45ab0b4 Mon Sep 17 00:00:00 2001
From: Scott Owens <sowens@fb.com>
Date: Thu, 29 Aug 2019 08:06:27 -0700
Subject: [PATCH] [sledge semantics] Add a rough draft llair semantics

Summary:
Not everything is here yet, and there is some confusion on what to do
about the size values. However, the semantics has the right general
shape and will be a nice starting point for thinking about the details.

Reviewed By: jberdine

Differential Revision: D17111041

fbshipit-source-id: cc75651c6
---
 sledge/semantics/llairScript.sml        | 337 ++++++++++++++++++++++--
 sledge/semantics/llvmScript.sml         |   5 +-
 sledge/semantics/memory_modelScript.sml |   3 +-
 3 files changed, 324 insertions(+), 21 deletions(-)

diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml
index e07e25385..e75a92971 100644
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@@ -115,7 +115,7 @@ Datatype:
 End
 
 Datatype:
-  llair = <| globals : global list; functions : (label, func) alist |>
+  llair = <| globals : global list; functions : (string, func) alist |>
 End
 
 (* ----- Semantic states ----- *)
@@ -134,42 +134,345 @@ End
 Type v = ``:flat_v reg_v``
 
 Datatype:
-  pc = <| l : label; i : num |>
-End
-
-Datatype:
-  frame = <| ret : pc; exn_ret : pc; ret_var : var; saved_locals : var |-> v; |>
+  frame = <| ret : label; exn_ret : label; ret_var : var; saved_locals : var |-> v; |>
 End
 
 Datatype:
   state =
-    <| ip : pc;
+    <| bp : label; (* Pointer to the next block to execute *)
        globals : var |-> word64;
        locals : var |-> v;
        stack : frame list;
+       pointer_size : 'a itself;
        heap : unit heap |>
 End
 
 (* ----- Semantic transitions ----- *)
 
-Definition eval_exp_def:
-  eval_exp = ARB: state -> exp -> v
+Definition sizeof_def:
+  (sizeof (:'a) (IntegerT n) = n) ∧
+  (sizeof (:'a) (PointerT t) = dimindex (:'a)) ∧
+  (sizeof (:'a) (ArrayT t n) = n * sizeof (:'a) t) ∧
+  (sizeof (:'a) (TupleT ts) = sum (map (sizeof (:'a)) ts))
+Termination
+  WF_REL_TAC `measure (typ_size o snd)` >> simp [] >>
+  Induct >> rw [definition "typ_size_def"] >> simp [] >>
+  first_x_assum drule >> decide_tac
+End
+
+Definition type_to_shape_def:
+  (type_to_shape (:'a) (IntegerT n) = Flat (sizeof (:'a) (IntegerT n)) (IntegerT n)) ∧
+  (type_to_shape (:'a) (ArrayT t n) = Array (type_to_shape (:'a) t) n) ∧
+  (type_to_shape (:'a) (TupleT ts) = Tuple (map (type_to_shape (:'a)) ts))
+Termination
+  WF_REL_TAC `measure (typ_size o snd)` >>
+  rw [] >>
+  Induct_on `ts` >> rw [definition "typ_size_def"] >>
+  res_tac >> decide_tac
+End
+
+Definition first_class_type_def:
+  (first_class_type (IntegerT _) ⇔ T) ∧
+  (first_class_type (PointerT _) ⇔ T) ∧
+  (first_class_type (ArrayT t _) ⇔ first_class_type t) ∧
+  (first_class_type (TupleT ts) ⇔ every first_class_type ts) ∧
+  (first_class_type _ ⇔ F)
+Termination
+  WF_REL_TAC `measure typ_size` >>
+  rw [] >>
+  Induct_on `ts` >> rw [definition "typ_size_def"] >>
+  res_tac >> decide_tac
+End
+
+Inductive value_type:
+  (value_type (IntegerT n) (FlatV (IntV i n))) ∧
+  (value_type (PointerT _) (FlatV (LocV n))) ∧
+  (every (value_type t) vs ∧ length vs = n ∧ first_class_type t
+   ⇒
+   value_type (ArrayT t n) (AggV vs)) ∧
+  (list_rel value_type ts vs
+   ⇒
+   value_type (StrT ts) (AggV vs))
+End
+
+Definition bool2v_def:
+  bool2v b = FlatV (IntV (if b then 1 else 0) 1)
+End
+
+Definition int2unsigned_def:
+  int2unsigned (i:int) size =
+    if i < 0 then
+      256 ** size + i
+    else
+      i
+End
+
+Definition fits_def:
+  fits (i:int) size ⇔
+    0 < size ∧ 0 - (256 ** (size - 1)) ≤ i ∧ i < 256 ** (size - 1)
+End
+
+(* TODO: We never create anything that is a SizeV *)
+Inductive eval_exp:
+  (∀s v r.
+   flookup s.locals v = Some r
+   ⇒
+   eval_exp s (Var v) r) ∧
+
+  (* TODO: Nondet I guess we need to know the type here *)
+  (* TODO: Label *)
+
+  (∀s e1 e2 size byte.
+   eval_exp s e1 (FlatV (IntV byte 1)) ∧
+   eval_exp s e2 (FlatV (SizeV size))
+   ⇒
+   eval_exp s (Splat e1 e2) (AggV (replicate size (FlatV (IntV byte 1))))) ∧
+
+   (* TODO Question: What if size <> vals? *)
+  (∀s e1 e2 size vals.
+   eval_exp s e1 (AggV vals) ∧
+   eval_exp s e2 (FlatV (SizeV size)) ∧
+   size = length vals
+   ⇒
+   eval_exp s (Memory e1 e2) (AggV vals)) ∧
+
+  (∀s es vals.
+   list_rel (eval_exp s) es (map AggV vals)
+   ⇒
+   eval_exp s (Concat es) (AggV (flat vals))) ∧
+
+  (∀s i size.
+   eval_exp s (Integer i (IntegerT size)) (FlatV (IntV i size))) ∧
+
+  (* TODO Question: Should the same integer with two different sizes be equal *)
+  (∀s e1 e2 r1 r2.
+   eval_exp s e1 r1 ∧
+   eval_exp s e2 r2
+   ⇒
+   eval_exp s (Eq e1 e2) (bool2v (r1 = r2))) ∧
+
+  (∀s e1 e2 i1 size1 i2 size2.
+   eval_exp s e1 (FlatV (IntV i1 size1)) ∧
+   eval_exp s e2 (FlatV (IntV i2 size2)) ∧
+   fits i1 size1 ∧
+   fits i2 size2
+   ⇒
+   eval_exp s (Lt e1 e2) (bool2v (i1 < i2))) ∧
+
+  (∀s e1 e2 i1 size1 i2 size2.
+   eval_exp s e1 (FlatV (IntV i1 size1)) ∧
+   eval_exp s e2 (FlatV (IntV i2 size2)) ∧
+   fits i1 size1 ∧
+   fits i2 size2
+   ⇒
+   eval_exp s (Ult e1 e2) (bool2v (int2unsigned i1 size1 < int2unsigned i2 size2))) ∧
+
+  (∀s size e1 e2 i1 i2.
+   eval_exp s e1 (FlatV (IntV i1 size)) ∧
+   eval_exp s e2 (FlatV (IntV i2 size)) ∧
+   fits i1 size ∧
+   fits i2 size
+   ⇒
+   eval_exp s (Sub (IntegerT size) e1 e2) (FlatV (IntV (i1 - i2) size))) ∧
+
+  (∀s es vals.
+   list_rel (eval_exp s) es vals
+   ⇒
+   eval_exp s (Record es) (AggV vals)) ∧
+
+  (∀s e1 e2 vals size.
+   eval_exp s e1 (AggV vals) ∧
+   eval_exp s e2 (FlatV (SizeV size)) ∧
+   size < length vals
+   ⇒
+   eval_exp s (Select e1 e2) (el size vals)) ∧
+
+  (∀s e1 e2 e3 vals size r.
+   eval_exp s e1 (AggV vals) ∧
+   eval_exp s e2 (FlatV (SizeV size)) ∧
+   eval_exp s e3 r ∧
+   size < length vals
+   ⇒
+   eval_exp s (Update e1 e2 e3) (AggV (list_update r size vals)))
+
+End
+
+Definition convert_value_def:
+  (convert_value (IntegerT n) w = IntV (w2i w) n) ∧
+  (convert_value (PointerT t) w = LocV (w2n w))
+End
+
+Definition bytes_to_llair_value_def:
+  bytes_to_llair_value (:'a) t bs =
+    (bytes_to_value (λn t (w:'a word). convert_value t w) (type_to_shape (:'a) t) bs)
+End
+
+Definition unconvert_value_def:
+  (unconvert_value (:'a) (IntV i size) = (size, i2w i)) ∧
+  (unconvert_value (:'a) (LocV n) = (dimindex (:'a), n2w n))
+End
+
+Definition llair_value_to_bytes_def:
+  llair_value_to_bytes (:'a) v =
+    value_to_bytes (unconvert_value (:'a) : flat_v -> num # 'a word) v
 End
 
 Definition update_results_def:
   update_results xvs s = s with locals := s.locals |++ xvs
 End
 
-Definition inc_pc_def:
-  inc_pc s = s with ip := (s.ip with i := s.ip.i + 1)
+Inductive step_inst:
+  (∀s ves r.
+    eval_exp s e r
+    ⇒
+    step_inst s
+    (Move ves)
+    (update_results (map (λ(v,e). (v, r)) ves) s)) ∧
+
+  (∀(s:'a state) x t e size ptr freeable interval bytes.
+   eval_exp s e (FlatV (LocV ptr)) ∧
+   interval = Interval freeable ptr (ptr + size) ∧
+   is_allocated interval s.heap ∧
+   bytes = map snd (get_bytes s.heap interval)
+   ⇒
+   step_inst s
+    (Load (Var_name x t) e size)
+    (update_results [(Var_name x t, fst (bytes_to_llair_value (:'a) t bytes))] s)) ∧
+
+  (∀s e1 e2 size ptr bytes freeable interval r.
+   eval_exp s e1 (FlatV (LocV ptr)) ∧
+   eval_exp s e2 r ∧
+   interval = Interval freeable ptr (ptr + size) ∧
+   is_allocated interval s.heap ∧
+   bytes = llair_value_to_bytes (:'a) r ∧
+   length bytes = size
+   ⇒
+   step_inst s
+     (Store e1 e2 size)
+     (s with heap := set_bytes () bytes ptr s.heap)) ∧
+
+  (* TODO memset *)
+
+  (∀s e1 e2 e3 dest_ptr src_ptr size src_interval freeable1 freeable2 bytes.
+   eval_exp s e1 (FlatV (LocV dest_ptr)) ∧
+   eval_exp s e2 (FlatV (LocV src_ptr)) ∧
+   eval_exp s e3 (FlatV (SizeV size)) ∧
+   src_interval = Interval freeable1 src_ptr (src_ptr + size) ∧
+   is_allocated src_interval s.heap ∧
+   is_allocated (Interval freeable2 dest_ptr (dest_ptr + size)) s.heap ∧
+   (* TODO Question: should we allow overlap? *)
+   bytes = map snd (get_bytes s.heap src_interval)
+   ⇒
+   step_inst s
+    (Memcpy e1 e2 e3)
+    (s with heap := set_bytes () bytes dest_ptr s.heap)) ∧
+
+  (* TODO memmove *)
+
+  (∀s v e1 e2 n size ptr new_h.
+   eval_exp s e1 (FlatV (SizeV n)) ∧
+   eval_exp s e2 (FlatV (SizeV size)) ∧
+   allocate s.heap (n * size) () (ptr, new_h)
+   ⇒
+   step_inst s
+     (Alloc v e1 e2)
+     (update_results [(v, FlatV (LocV ptr))] (s with heap := new_h))) ∧
+
+  (∀s e ptr.
+   eval_exp s e (FlatV (LocV ptr))
+   ⇒
+   step_inst s
+     (Free e)
+     (s with heap := deallocate [A ptr] s.heap)) ∧
+
+  (∀s x t nondet.
+   value_type t nondet
+   ⇒
+   step_inst s
+     (NondetI (Var_name x t))
+     (update_results [(Var_name x t, nondet)] s))
+
 End
 
-(*
-Inductive step_inst:
-  (step_inst (prog : llair) s
-    (Assign ves)
-    (inc_pc (update_results (map (λ(v,e). (v, eval_exp s e)) ves) s)))
+Inductive step_term:
+
+  (∀prog s e table default size fname bname bname'.
+   eval_exp s e (FlatV (SizeV size)) ∧
+   Lab_name fname bname = (case alookup table size of Some lab => lab | None => default) ∧
+   s.bp = Lab_name fname bname'
+   ⇒
+   step_term prog s
+     (Switch e table default)
+     (s with bp := Lab_name fname bname)) ∧
+
+  (∀prog s e labs size.
+   eval_exp s e (FlatV (SizeV size)) ∧
+   size < length labs
+   ⇒
+   step_term prog s
+     (Iswitch e labs)
+     (s with bp := el size labs)) ∧
+
+  (∀prog s v fname bname es t ret1 ret2 vals f.
+   alookup prog.functions fname = Some f ∧
+   f.entry = Lab_name fname bname ∧
+   list_rel (eval_exp s) es vals
+   ⇒
+   step_term prog s
+     (Call v (Lab_name fname bname) es t ret1 ret2)
+     <| bp := Lab_name fname bname;
+        globals := s.globals;
+        locals := alist_to_fmap (zip (f.params, vals));
+        stack :=
+          <| ret := ret1;
+             exn_ret := ret2;
+             ret_var := v;
+             saved_locals := s.locals |> :: s.stack;
+        pointer_size := s.pointer_size;
+        heap := s.heap |>) ∧
+
+  (∀prog s e r top rest.
+   eval_exp s e r ∧
+   s.stack = top::rest
+   ⇒
+   step_term prog s
+     (Return e)
+     <| bp := top.ret;
+        globals := s.globals;
+        locals := top.saved_locals |+ (top.ret_var, r);
+        stack := rest;
+        pointer_size := s.pointer_size;
+        heap := s.heap |>)
+
+  (* TODO Throw *)
+
+End
+
+(* With function calls terminating blocks, it's very easy to get rid of the
+ * instruction pointer and do a big-step evaluation for each block *)
+Inductive step_block:
+
+  (!prog s1 t s2.
+   step_term prog s1 t s2
+   ⇒
+   step_block prog s1 [] t s2) ∧
+
+  (!prog s1 i is t s2 s3.
+   step_inst s1 i s2 ∧
+   step_block prog s2 is t s3
+   ⇒
+   step_block prog s1 (i::is) t s3)
+
+End
+
+Inductive step:
+  (∀prog s fname bname f b s'.
+   s.bp = Lab_name fname bname ∧
+   alookup prog.functions fname = Some f ∧
+   alookup f.cfg s.bp = Some b ∧
+   step_block prog s b.cmnd b.term s'
+   ⇒
+   step prog s s')
 End
-*)
 
 export_theory ();
diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index d77e35485..cdd24bc8f 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -497,11 +497,12 @@ Inductive step_instr:
 
   (eval s a1 = v ∧
    v2n v.value = Some n ∧
-   allocate s.heap (n * sizeof t) v.poison (v2, new_h)
+   allocate s.heap (n * sizeof t) v.poison (n2, new_h)
    ⇒
    step_instr prog s
      (Alloca r t (t1, a1))
-     (inc_pc (update_result r v2 (s with heap := new_h)))) ∧
+     (inc_pc (update_result r <| poison := v.poison; value := FlatV (PtrV (n2w n2)) |>
+                (s with heap := new_h)))) ∧
 
   (eval s a1 = <| poison := p1; value := FlatV (PtrV w) |> ∧
    interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧
diff --git a/sledge/semantics/memory_modelScript.sml b/sledge/semantics/memory_modelScript.sml
index af9f49f69..549be0955 100644
--- a/sledge/semantics/memory_modelScript.sml
+++ b/sledge/semantics/memory_modelScript.sml
@@ -153,7 +153,6 @@ Definition get_bytes_def:
     map
       (λoff.
         case flookup h.memory (A (start + off)) of
-        | None => (F, 0w)
         | Some w => w)
       (count_list (stop - start))
 End
@@ -170,7 +169,7 @@ Inductive allocate:
    is_free b h ∧
    length bytes = size
    ⇒
-   allocate h size tag (w, set_bytes tag bytes p
+   allocate h size tag (p, set_bytes tag bytes p
                            <| memory := h.memory;
                               allocations := { b } ∪ h.allocations;
                               valid_addresses := h.valid_addresses |>)