Add types to the variable syntax in llair

Summary:
Each variable now contains its type, alongside its name. This is more
uniform than in LLVM, where the name is usually paired with a type, but
not always, for example, the register type of the result of an
extractvalue is left implicit.

Reviewed By: jberdine

Differential Revision: D16984630

fbshipit-source-id: 1c3bc4985

sledge/semantics/llairScript.sml

@@ -26,7 +26,7 @@ Datatype:
 End
 
 Datatype:
-  var = Var_name string
+  var = Var_name string typ
 End
 
 Datatype:

sledge/semantics/llvmScript.sml

@@ -81,7 +81,7 @@ Datatype:
   | Alloca reg ty targ
   | Load reg ty targ
   | Store targ targ
-  | Gep reg targ (targ list)
+  | Gep reg ty targ (targ list)
   | Ptrtoint reg targ ty
   | Inttoptr reg targ ty
   | Icmp reg cond ty arg arg
@@ -119,7 +119,7 @@ End
 Datatype:
   def =
     <| r : ty;
-       params : reg list;
+       params : (ty # reg) list;
        (* None -> entry block, and Some name -> non-entry block *)
        blocks : (label option, block) alist |>
 End
@@ -468,6 +468,21 @@ Definition do_phi_def:
     option_map (λarg. (id, eval s arg)) (alookup entries from_l)
 End
 
+Definition extract_type_def:
+  (extract_type t [] = Some t) ∧
+  (extract_type (ArrT n t) (i::idx) =
+    if i < n then
+      extract_type t idx
+    else
+      None) ∧
+  (extract_type (StrT ts) (i::idx) =
+    if i < length ts then
+      extract_type (el i ts) idx
+    else
+      None) ∧
+  (extract_type _ _ = None)
+End
+
 Definition extract_value_def:
   (extract_value v [] = Some v) ∧
   (extract_value (AggV vs) (i::indices) =
@@ -598,7 +613,7 @@ Inductive step_instr:
    get_offset t1 ns = Some off
    ⇒
    step_instr prog s
-    (Gep r ((PtrT t1), a1) tindices)
+    (Gep r t ((PtrT t1), a1) tindices)
     (inc_pc (update_result r
                <| poison := (v1.poison ∨ i1.poison ∨ exists (λv. v.poison) indices);
                   value := PtrV (n2w (w2n w1 + sizeof t1 * n + off)) |>
@@ -628,7 +643,7 @@ Inductive step_instr:
    step_instr prog s
      (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));
+        locals := alist_to_fmap (zip (map snd d.params, map (eval s o snd) targs));
         globals := s.globals;
         allocations:= s.allocations;
         stack :=

sledge/semantics/llvm_propScript.sml

@@ -475,21 +475,6 @@ Definition indices_in_range_def:
   (indices_in_range _ _ ⇔ F)
 End
 
-Definition extract_type_def:
-  (extract_type t [] = Some t) ∧
-  (extract_type (ArrT n t) (i::idx) =
-    if i < n then
-      extract_type t idx
-    else
-      None) ∧
-  (extract_type (StrT ts) (i::idx) =
-    if i < length ts then
-      extract_type (el i ts) idx
-    else
-      None) ∧
-  (extract_type _ _ = None)
-End
-
 (* The strict inequality does not hold because of 0 length arrays *)
 Theorem offset_size_leq:
   ∀t indices n.

sledge/semantics/llvm_to_llairScript.sml

@@ -67,11 +67,11 @@ Definition translate_ty_def:
 End
 
 Definition translate_glob_var_def:
-  translate_glob_var (Glob_var g) = Var_name g
+  translate_glob_var (Glob_var g) t = Var_name g (translate_ty t)
 End
 
 Definition translate_reg_def:
-  translate_reg (Reg r) = Var_name r
+  translate_reg (Reg r) t = Var_name r (translate_ty t)
 End
 
 Definition translate_label_def:
@@ -84,7 +84,8 @@ Definition translate_const_def:
     Record (map (λ(ty, c). translate_const c) tcs)) ∧
   (translate_const (ArrC tcs) =
     Record (map (λ(ty, c). translate_const c) tcs)) ∧
-  (translate_const (GlobalC g) = Var (translate_glob_var g)) ∧
+  (* TODO *)
+  (translate_const (GlobalC g) = Var (translate_glob_var g ARB)) ∧
   (* TODO *)
   (translate_const (GepC _ _ _ _) = ARB) ∧
   (translate_const UndefC = Nondet)
@@ -95,10 +96,10 @@ Termination
 End
 
 Definition translate_arg_def:
-  (translate_arg emap (Constant c) = translate_const c) ∧
+  (translate_arg emap (Constant c) t = translate_const c) ∧
-  (translate_arg emap (Variable r) =
+  (translate_arg emap (Variable r) t =
     case flookup emap r of
-    | None => Var (translate_reg r)
+    | None => Var (translate_reg r t)
     | Some e => e)
 End
 
@@ -112,11 +113,11 @@ End
 (* TODO *)
 Definition translate_instr_to_exp_def:
   (translate_instr_to_exp emap (llvm$Sub _ _ _ ty a1 a2) =
-    llair$Sub (translate_ty ty) (translate_arg emap a1) (translate_arg emap a2)) ∧
+    llair$Sub (translate_ty ty) (translate_arg emap a1 ty) (translate_arg emap a2 ty)) ∧
-  (translate_instr_to_exp emap (Extractvalue _ (_, a) cs) =
+  (translate_instr_to_exp emap (Extractvalue _ (t, a) cs) =
-    foldl (λe c. Select e (translate_const c)) (translate_arg emap a) cs) ∧
+    foldl (λe c. Select e (translate_const c)) (translate_arg emap a t) cs) ∧
-  (translate_instr_to_exp emap (Insertvalue _ (_, a1) (_, a2) cs) =
+  (translate_instr_to_exp emap (Insertvalue _ (t1, a1) (t2, a2) cs) =
-    translate_updatevalue (translate_arg emap a1) (translate_arg emap a2) cs)
+    translate_updatevalue (translate_arg emap a1 t1) (translate_arg emap a2 t2) cs)
 End
 
 (* This translation of insertvalue to update and select is quadratic in the
@@ -169,25 +170,39 @@ End
 (* TODO *)
 Definition translate_instr_to_inst_def:
   (translate_instr_to_inst emap (llvm$Store (t1, a1) (t2, a2)) =
-    llair$Store (translate_arg emap a1) (translate_arg emap a2) (sizeof t2)) ∧
+    llair$Store (translate_arg emap a1 t1) (translate_arg emap a2 t2) (sizeof t2)) ∧
   (translate_instr_to_inst emap (Load r t (t1, a1)) =
-    Load (translate_reg r) (translate_arg emap a1) (sizeof t))
+    Load (translate_reg r t1) (translate_arg emap a1 t1) (sizeof t))
 End
 
 (* TODO *)
 Definition translate_instr_to_term_def:
   translate_instr_to_term f emap (Br a l1 l2) =
-    Iswitch (translate_arg emap a) [translate_label f l2; translate_label f l1]
+    Iswitch (translate_arg emap a (IntT W1)) [translate_label f l2; translate_label f l1]
 End
 
 Datatype:
   instr_class =
-  | Exp reg
+  | Exp reg ty
   | Non_exp
   | Term
   | Call
 End
 
+(* Convert index lists as for GEP into number lists, for the purpose of
+ * calculating types. Everything goes to 0 but for positive integer constants,
+ * because those things can't be used to index anything but arrays, and the type
+ * for the array contents doesn't depend on the index's value. *)
+Definition idx_to_num_def:
+  (idx_to_num (_, (Constant (IntC _ n))) = Num (ABS n)) ∧
+  (idx_to_num (_, _) = 0)
+End
+
+Definition cidx_to_num_def:
+  (cidx_to_num (IntC _ n) = Num (ABS n)) ∧
+  (cidx_to_num _ = 0)
+End
+
 Definition classify_instr_def:
   (classify_instr (Call _ _ _ _) = Call) ∧
   (classify_instr (Ret _) = Term) ∧
@@ -199,16 +214,19 @@ Definition classify_instr_def:
   (classify_instr (Cxa_throw _ _ _) = Non_exp) ∧
   (classify_instr Cxa_end_catch = Non_exp) ∧
   (classify_instr (Cxa_begin_catch _ _) = Non_exp) ∧
-  (classify_instr (Sub r _ _ _ _ _) = Exp r) ∧
+  (classify_instr (Sub r _ _ t _ _) = Exp r t) ∧
-  (classify_instr (Extractvalue r _ _) = Exp r) ∧
+  (classify_instr (Extractvalue r (t, _) idx) =
-  (classify_instr (Insertvalue r _ _ _) = Exp r) ∧
+    Exp r (THE (extract_type t (map cidx_to_num idx)))) ∧
-  (classify_instr (Alloca r _ _) = Exp r) ∧
+  (classify_instr (Insertvalue r (t, _) _ idx) = Exp r t) ∧
-  (classify_instr (Gep r _ _) = Exp r) ∧
+  (classify_instr (Alloca r t _) = Exp r (PtrT t)) ∧
-  (classify_instr (Ptrtoint r _ _) = Exp r) ∧
+  (classify_instr (Gep r t _ idx) =
-  (classify_instr (Inttoptr r _ _) = Exp r) ∧
+    Exp r (PtrT (THE (extract_type t (map idx_to_num idx))))) ∧
-  (classify_instr (Icmp r _ _ _ _) = Exp r) ∧
+  (classify_instr (Ptrtoint r _ t) = Exp r t) ∧
-  (classify_instr (Cxa_allocate_exn r _) = Exp r) ∧
+  (classify_instr (Inttoptr r _ t) = Exp r t) ∧
-  (classify_instr (Cxa_get_exception_ptr r _) = Exp r)
+  (classify_instr (Icmp r _ _ _ _) = Exp r (IntT W1)) ∧
+  (* TODO *)
+  (classify_instr (Cxa_allocate_exn r _) = Exp r ARB) ∧
+  (classify_instr (Cxa_get_exception_ptr r _) = Exp r ARB)
 End
 
 (* Translate a list of instructions into an block. f is the name of the function
@@ -235,8 +253,8 @@ Definition translate_instrs_def:
   (translate_instrs f live_out emap [] = <| cmnd := []; term := Unreachable |>) ∧
   (translate_instrs f live_out emap (i :: is) =
     case classify_instr i of
-    | Exp r =>
+    | Exp r t =>
-      let x = translate_reg r in
+      let x = translate_reg r t in
       let e = translate_instr_to_exp emap i in
         if r ∈ live_out then
           let b = translate_instrs f live_out (emap |+ (r, Var x)) is in
@@ -257,7 +275,7 @@ Definition dest_label_def:
 End
 
 Definition dest_phi_def:
-  dest_phi (Phi r _ largs) = (r, largs)
+  dest_phi (Phi r t largs) = (r, t, largs)
 End
 
 Definition translate_label_opt_def:
@@ -269,9 +287,9 @@ Definition translate_header_def:
   (translate_header f entry Entry = []) ∧
   (translate_header f entry (Head phis _) =
     map
-      (λ(r, largs).
+      (λ(r, t, largs).
-        (translate_reg r,
+        (translate_reg r t,
-         map (λ(l, arg). (translate_label_opt f entry l, translate_arg fempty arg)) largs))
+         map (λ(l, arg). (translate_label_opt f entry l, translate_arg fempty arg t)) largs))
       (map dest_phi phis))
 End
 
@@ -333,12 +351,16 @@ Definition remove_phis_def:
   remove_phis f used_names bs = flat (snd (generate_move_blocks_list f used_names bs bs))
 End
 
+Definition translate_param_def:
+  translate_param (t, r) = translate_reg r t
+End
+
 Definition translate_def_def:
   translate_def (Lab f) d =
     let used_names = ARB in
     let entry_name = gen_name used_names "entry" in
     let bs = map (translate_block f entry_name UNIV) d.blocks in
-      <| params := map translate_reg d.params;
+      <| params := map translate_param d.params;
         (* TODO: calculate these from the produced llair, and not the llvm *)
         locals := ARB;
         entry := Lab_name f entry_name;