Theory VIMP_Expr

theory VIMP_Expr
  imports VIMP_Syntax
begin

section ‹Expression evaluation›

text ‹
  ‹aval› evaluates an expression in a store.  Every VIMP expression is integer-valued, so
  there is no separate Boolean type. Conditions use C-style truthiness (non-zero),
  while comparisons and logical operators yield ‹1› or ‹0›.  Evaluation is total and has no
  effects, which is why a guard can be re-evaluated freely by the transfer functions.
›

text ‹Division and remainder truncate toward zero for non-zero divisors.
  VIMP keeps expressions total by defining division by zero as zero and
  remainder by zero as the dividend. These zero-divisor cases are VIMP
  conventions; they do not model C's undefined behavior.›

definition c_div :: "int ⇒ int ⇒ int" where
  "c_div a b =
    (if b = 0 then 0 else sgn a * sgn b * (abs a div abs b))"

definition c_mod :: "int ⇒ int ⇒ int" where
  "c_mod a b = (if b = 0 then a else a - c_div a b * b)"

lemma c_div_zero [simp]: "c_div a 0 = 0" "c_div 0 b = 0"
  by (simp_all add: c_div_def)

lemma c_mod_zero [simp]: "c_mod a 0 = a" "c_mod 0 b = 0"
  by (simp_all add: c_mod_def)

lemma c_div_one [simp]: "c_div a 1 = a" "c_div a (-1) = -a"
  by (simp_all add: c_div_def sgn_mult_abs)

lemma c_mod_one [simp]: "c_mod a 1 = 0" "c_mod a (-1) = 0"
  by (simp_all add: c_mod_def)

lemma c_div_mod_reconstruct:
  "c_div a b * b + c_mod a b = a"
  by (simp add: c_mod_def)

lemma c_mod_abs:
  "c_mod a b = sgn a * (abs a mod abs b)"
proof (cases "b = 0")
  case True
  then show ?thesis by (simp add: sgn_mult_abs)
next
  case False
  have product: "c_div a b * b = sgn a * (abs a div abs b * abs b)"
    using False unfolding c_div_def
    by (simp add: abs_sgn mult_ac)
  have "sgn a * (abs a div abs b * abs b) + sgn a * (abs a mod abs b) = a"
    by (simp only: distrib_left[symmetric] div_mult_mod_eq sgn_mult_abs)
  with False product show ?thesis unfolding c_mod_def by (simp only: False if_False; linarith)
qed

lemma c_div_exact:
  assumes "b dvd a"
  shows "c_div a b = a div b"
proof (cases "b = 0")
  case True
  with assms show ?thesis by simp
next
  case False
  have rem: "c_mod a b = 0"
    using assms by (simp add: c_mod_abs)
  have product: "c_div a b * b = a"
    using c_div_mod_reconstruct[of a b] rem by simp
  have "c_div a b = (c_div a b * b) div b"
    using False by simp
  also have "... = a div b" using product by simp
  finally show ?thesis .
qed

lemma c_div_nonneg:
  "0 ≤ a ⟹ 0 ≤ b ⟹ 0 ≤ c_div a b"
  "a ≤ 0 ⟹ b ≤ 0 ⟹ 0 ≤ c_div a b"
  by (auto simp: c_div_def sgn_if pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)

lemma c_div_nonpos:
  "a ≤ 0 ⟹ 0 ≤ b ⟹ c_div a b ≤ 0"
  "0 ≤ a ⟹ b ≤ 0 ⟹ c_div a b ≤ 0"
  by (auto simp: c_div_def sgn_if pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)

lemma c_mod_nonneg:
  "0 ≤ a ⟹ 0 ≤ c_mod a b"
  by (cases "b = 0") (auto simp: c_mod_abs sgn_if intro: pos_mod_sign)

lemma c_mod_nonpos:
  "a ≤ 0 ⟹ c_mod a b ≤ 0"
  by (cases "b = 0") (auto simp: c_mod_abs sgn_if intro: pos_mod_sign)

lemma c_div_neg_divisor:
  "c_div a (-b) = - c_div a b"
  by (simp add: c_div_def)

lemma c_div_neg_dividend:
  "c_div (-a) b = - c_div a b"
  by (simp add: c_div_def)

definition truthy :: "int ⇒ bool" where
  [simp]: "truthy n ⟷ n ≠ 0"

fun aval :: "exp ⇒ store ⇒ int" ("⟦_⟧⇩e") where
    "⟦N n⟧⇩e     s  = n"
  | "⟦V x⟧⇩e     s  = s x"
  | "⟦Plus  a b⟧⇩e s  = ⟦a⟧⇩e s + ⟦b⟧⇩e s"
  | "⟦Minus a b⟧⇩e s  = ⟦a⟧⇩e s - ⟦b⟧⇩e s"
  | "⟦Times a b⟧⇩e s  = ⟦a⟧⇩e s * ⟦b⟧⇩e s"
  | "⟦Div a b⟧⇩e s = c_div (⟦a⟧⇩e s) (⟦b⟧⇩e s)"
  | "⟦Mod a b⟧⇩e s = c_mod (⟦a⟧⇩e s) (⟦b⟧⇩e s)"
  | "⟦Less a b⟧⇩e  s  = (if ⟦a⟧⇩e s < ⟦b⟧⇩e s then 1 else 0)"
  | "⟦LessEq a b⟧⇩e s = (if ⟦a⟧⇩e s ≤ ⟦b⟧⇩e s then 1 else 0)"
  | "⟦Greater a b⟧⇩e s = (if ⟦a⟧⇩e s > ⟦b⟧⇩e s then 1 else 0)"
  | "⟦GreaterEq a b⟧⇩e s = (if ⟦a⟧⇩e s ≥ ⟦b⟧⇩e s then 1 else 0)"
  | "⟦NotEq a b⟧⇩e s = (if ⟦a⟧⇩e s ≠ ⟦b⟧⇩e s then 1 else 0)"
  | "⟦Eq   a b⟧⇩e  s  = (if ⟦a⟧⇩e s = ⟦b⟧⇩e s then 1 else 0)"
  | "⟦Not b⟧⇩e     s  = (if truthy (⟦b⟧⇩e s) then 0 else 1)"
  | "⟦And b1 b2⟧⇩e s  = (if truthy (⟦b1⟧⇩e s) ∧ truthy (⟦b2⟧⇩e s) then 1 else 0)"
  | "⟦Or  b1 b2⟧⇩e s  = (if truthy (⟦b1⟧⇩e s) ∨ truthy (⟦b2⟧⇩e s) then 1 else 0)"

text ‹
  ‹truthy› of a compiled comparison or Boolean expression restated in plain
  Boolean form, so a caller never has to re-derive it from ‹aval.simps› and
  ‹truthy›'s own ‹≠ 0› encoding through an explicit ‹if›-split.
›

lemma truthy_aval_Less [simp]:
  "truthy (⟦Less a b⟧⇩e s) ⟷ ⟦a⟧⇩e s < ⟦b⟧⇩e s"
  by simp

lemma truthy_aval_LessEq [simp]:
  "truthy (⟦LessEq a b⟧⇩e s) ⟷ ⟦a⟧⇩e s ≤ ⟦b⟧⇩e s"
  by simp

lemma truthy_aval_Greater [simp]:
  "truthy (⟦Greater a b⟧⇩e s) ⟷ ⟦a⟧⇩e s > ⟦b⟧⇩e s"
  by simp

lemma truthy_aval_GreaterEq [simp]:
  "truthy (⟦GreaterEq a b⟧⇩e s) ⟷ ⟦a⟧⇩e s ≥ ⟦b⟧⇩e s"
  by simp

lemma truthy_aval_NotEq [simp]:
  "truthy (⟦NotEq a b⟧⇩e s) ⟷ ⟦a⟧⇩e s ≠ ⟦b⟧⇩e s"
  by simp

lemma truthy_aval_Eq [simp]:
  "truthy (⟦Eq a b⟧⇩e s) ⟷ ⟦a⟧⇩e s = ⟦b⟧⇩e s"
  by simp

lemma truthy_aval_Not [simp]:
  "truthy (⟦Not b⟧⇩e s) ⟷ ¬ truthy (⟦b⟧⇩e s)"
  by simp

lemma truthy_aval_And [simp]:
  "truthy (⟦And b1 b2⟧⇩e s) ⟷ truthy (⟦b1⟧⇩e s) ∧ truthy (⟦b2⟧⇩e s)"
  by simp

lemma truthy_aval_Or [simp]:
  "truthy (⟦Or b1 b2⟧⇩e s) ⟷ truthy (⟦b1⟧⇩e s) ∨ truthy (⟦b2⟧⇩e s)"
  by simp

subsection ‹Finite expression footprints›

text ‹The variables an expression mentions. A transfer that evaluates the
  expression needs no other variable, which is what lets a keyed analysis read
  only the globals an edge mentions.›

fun exp_vnames :: "exp ⇒ vname set" where
  "exp_vnames (N _) = {}"
| "exp_vnames (V x) = {x}"
| "exp_vnames (Plus a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (Minus a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (Times a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (Div a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (Mod a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (Less a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (LessEq a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (Greater a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (GreaterEq a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (NotEq a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (Eq a b) = exp_vnames a ∪ exp_vnames b"
| "exp_vnames (Not b) = exp_vnames b"
| "exp_vnames (And b1 b2) = exp_vnames b1 ∪ exp_vnames b2"
| "exp_vnames (Or b1 b2) = exp_vnames b1 ∪ exp_vnames b2"

lemma finite_exp_vnames [simp]: "finite (exp_vnames a)"
  by (induction a) auto

end