[sledge sem] Fix the semantics and trans. of If

Summary:
The LLVM semantics and translation was not consistently treating the
1-bit word value condition as signed or unsigned.

Reviewed By: jberdine

Differential Revision: D17605766

fbshipit-source-id: 77edf63b7

sledge/semantics/llairScript.sml

@@ -85,7 +85,7 @@ End
 Datatype:
   term =
   (* Args: key, branch table, default exp *)
-  | Switch exp ((num # label) list) label
+  | Switch exp ((int # label) list) label
   (* Args: int to switch on, jump table *)
   | Iswitch exp (label list)
   (* Args:  result reg, function to call, arguments, return type of callee,
@@ -428,10 +428,9 @@ End
 
 Inductive step_term:
 
-  (∀prog s e table default idx fname bname bname' idx_size.
-   eval_exp s e (FlatV (IntV (&idx) idx_size)) ∧
-   Lab_name fname bname = (case alookup table idx of Some lab => lab | None => default) ∧
-   s.bp = Lab_name fname bname'
+  (∀prog s e table default idx fname bname idx_size.
+   eval_exp s e (FlatV (IntV idx idx_size)) ∧
+   Lab_name fname bname = (case alookup table idx of Some lab => lab | None => default)
    ⇒
    step_term prog s
      (Switch e table default)

sledge/semantics/llvmScript.sml

@@ -514,7 +514,7 @@ Inductive step_instr:
           heap := new_h |>)) ∧
 
   (eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧
-   l = Some (if tf = 1w then l1 else l2)
+   l = Some (if tf = 0w then l2 else l1)
    ⇒
    step_instr prog s
      (Br a l1 l2) Tau
@@ -713,7 +713,7 @@ End
  * *)
 Definition sem_def:
   sem p s1 =
-    { (get_observation p (last path), filter (\x. x ≠ Tau) l)  | (path, l) |
+    { (get_observation p (last path), filter ($≠ Tau) l)  | (path, l) |
       toList (labels path) = Some l ∧ finite path ∧ okpath (step p) path ∧ first path = s1 }
 End
 

sledge/semantics/llvm_propScript.sml

@@ -799,7 +799,7 @@ Theorem find_path_prefix:
     obs ∈ observation_prefixes (get_observation p (last path), l1)
     ⇒
     ∃n l2. n ∈ PL path ∧ toList (labels (take n path)) = Some l2 ∧
-      obs = (get_observation p (last (take n path)), filter (\x. x ≠ Tau) l2)
+      obs = (get_observation p (last (take n path)), filter ($≠ Tau) l2)
 Proof
   ho_match_mp_tac finite_okpath_ind >> rw [toList_THM]
   >- fs [observation_prefixes_cases, get_observation_def, IN_DEF] >>
@@ -825,7 +825,7 @@ Proof
     metis_tac [exit_no_step]) >>
   rename1 `short_l ≼ long_l` >>
   rfs [] >>
-  `(Partial, filter (\x. x ≠ Tau) short_l) ∈ observation_prefixes (get_observation p (last path),long_l)`
+  `(Partial, filter ($≠ Tau) short_l) ∈ observation_prefixes (get_observation p (last path),long_l)`
   by (simp [observation_prefixes_cases, IN_DEF] >> metis_tac []) >>
   first_x_assum drule >> strip_tac >>
   qexists_tac `Suc n` >> simp [toList_THM] >> rw [] >> rfs [last_take]
@@ -848,7 +848,7 @@ Proof
     `?n short_l.
       n ∈ PL s_path ∧
       toList (labels (take n s_path)) = Some short_l ∧
-      x = (get_observation p (last (take n s_path)), filter (\x. x ≠ Tau) short_l)`
+      x = (get_observation p (last (take n s_path)), filter ($≠ Tau) short_l)`
     by metis_tac [find_path_prefix] >>
     qexists_tac `take n s_path` >> rw [])
   >- (

sledge/semantics/llvm_to_llairScript.sml

@@ -188,7 +188,7 @@ 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]
+    Switch (translate_arg emap a) [(0, translate_label f l2)] (translate_label f l1)
 End
 
 Datatype:
@@ -219,6 +219,7 @@ Definition classify_instr_def:
   (classify_instr (Br _ _ _) = Term) ∧
   (classify_instr (Invoke _ _ _ _ _ _) = Term) ∧
   (classify_instr Unreachable = Term) ∧
+  (classify_instr Exit = Term) ∧
   (classify_instr (Load _ _ _) = Non_exp) ∧
   (classify_instr (Store _ _) = Non_exp) ∧
   (classify_instr (Cxa_throw _ _ _) = Non_exp) ∧

sledge/semantics/miscScript.sml

@@ -35,12 +35,12 @@ Datatype:
 End
 
 Inductive observation_prefixes:
-  (∀l. observation_prefixes (Complete, l) (Complete, filter (\x. x ≠ Tau) l)) ∧
-  (∀l. observation_prefixes (Stuck, l) (Stuck, filter (\x. x ≠ Tau) l)) ∧
+  (∀l. observation_prefixes (Complete, l) (Complete, filter ($≠ Tau) l)) ∧
+  (∀l. observation_prefixes (Stuck, l) (Stuck, filter ($≠ Tau) l)) ∧
   (∀l1 l2 x.
     l2 ≼ l1 ∧ (l2 = l1 ⇒ x = Partial)
     ⇒
-    observation_prefixes (x, l1) (Partial, filter (\x. x ≠ Tau) l2))
+    observation_prefixes (x, l1) (Partial, filter ($≠ Tau) l2))
 End
 
 (* ----- Theorems about list library functions ----- *)
@@ -645,4 +645,17 @@ Proof
   metis_tac [unfold_finite_funpow, opt_funpow_def]
 QED
 
+(* ----- pred_set theorems ----- *)
+
+Theorem drestrict_union_eq:
+  !m1 m2 s1 s2.
+    DRESTRICT m1 (s1 ∪ s2) = DRESTRICT m2 (s1 ∪ s2)
+    ⇔
+    DRESTRICT m1 s1 = DRESTRICT m2 s1 ∧
+    DRESTRICT m1 s2 = DRESTRICT m2 s2
+Proof
+  rw [DRESTRICT_EQ_DRESTRICT_SAME] >> eq_tac >> rw [] >> fs [EXTENSION] >>
+  metis_tac []
+QED
+
 export_theory ();