From 71aa4816d64ab4d06c85ae0f41f140445f1f646c Mon Sep 17 00:00:00 2001 From: Scott Owens Date: Fri, 27 Sep 2019 02:15:32 -0700 Subject: [PATCH] [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 | 9 ++++----- sledge/semantics/llvmScript.sml | 4 ++-- sledge/semantics/llvm_propScript.sml | 6 +++--- sledge/semantics/llvm_to_llairScript.sml | 3 ++- sledge/semantics/miscScript.sml | 19 ++++++++++++++++--- 5 files changed, 27 insertions(+), 14 deletions(-) diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml index 254fc96d9..36d04ba55 100644 --- a/sledge/semantics/llairScript.sml +++ b/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) diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml index 8027b9bd4..22c130866 100644 --- a/sledge/semantics/llvmScript.sml +++ b/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 diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml index a5f199b78..6f4af157f 100644 --- a/sledge/semantics/llvm_propScript.sml +++ b/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 []) >- ( diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml index 3b21f0702..9c5d255fd 100644 --- a/sledge/semantics/llvm_to_llairScript.sml +++ b/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) ∧ diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml index a17ff8e9e..e5092ed21 100644 --- a/sledge/semantics/miscScript.sml +++ b/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 ();