Semantics for shift operations

Author: BraeWebb

Graph/IRNodeHierarchy.thy

@@ -29,8 +29,11 @@ fun is_VirtualState :: "IRNode \<Rightarrow> bool" where
 fun is_BinaryArithmeticNode :: "IRNode \<Rightarrow> bool" where
   "is_BinaryArithmeticNode n = ((is_AddNode n) \<or> (is_AndNode n) \<or> (is_MulNode n) \<or> (is_OrNode n) \<or> (is_SubNode n) \<or> (is_XorNode n))"
 
+fun is_ShiftNode :: "IRNode \<Rightarrow> bool" where
+  "is_ShiftNode n = ((is_LeftShiftNode n) \<or> (is_RightShiftNode n) \<or> (is_UnsignedRightShiftNode n))"
+
 fun is_BinaryNode :: "IRNode \<Rightarrow> bool" where
-  "is_BinaryNode n = ((is_BinaryArithmeticNode n))"
+  "is_BinaryNode n = ((is_BinaryArithmeticNode n) \<or> (is_ShiftNode n))"
 
 fun is_AbstractLocalNode :: "IRNode \<Rightarrow> bool" where
   "is_AbstractLocalNode n = ((is_ParameterNode n))"
@@ -135,7 +138,7 @@ fun is_MemoryKill :: "IRNode \<Rightarrow> bool" where
   "is_MemoryKill n = ((is_AbstractMemoryCheckpoint n))"
 
 fun is_NarrowableArithmeticNode :: "IRNode \<Rightarrow> bool" where
-  "is_NarrowableArithmeticNode n = ((is_AbsNode n) \<or> (is_AddNode n) \<or> (is_AndNode n) \<or> (is_MulNode n) \<or> (is_NegateNode n) \<or> (is_NotNode n) \<or> (is_OrNode n) \<or> (is_SubNode n) \<or> (is_XorNode n))"
+  "is_NarrowableArithmeticNode n = ((is_AbsNode n) \<or> (is_AddNode n) \<or> (is_AndNode n) \<or> (is_MulNode n) \<or> (is_NegateNode n) \<or> (is_NotNode n) \<or> (is_OrNode n) \<or> (is_ShiftNode n) \<or> (is_SubNode n) \<or> (is_XorNode n))"
 
 fun is_AnchoringNode :: "IRNode \<Rightarrow> bool" where
   "is_AnchoringNode n = ((is_AbstractBeginNode n))"
@@ -180,7 +183,7 @@ fun is_GuardedNode :: "IRNode \<Rightarrow> bool" where
   "is_GuardedNode n = ((is_FloatingGuardedNode n))"
 
 fun is_ArithmeticLIRLowerable :: "IRNode \<Rightarrow> bool" where
-  "is_ArithmeticLIRLowerable n = ((is_AbsNode n) \<or> (is_BinaryArithmeticNode n) \<or> (is_IntegerConvertNode n) \<or> (is_NotNode n) \<or> (is_UnaryArithmeticNode n))"
+  "is_ArithmeticLIRLowerable n = ((is_AbsNode n) \<or> (is_BinaryArithmeticNode n) \<or> (is_IntegerConvertNode n) \<or> (is_NotNode n) \<or> (is_ShiftNode n) \<or> (is_UnaryArithmeticNode n))"
 
 fun is_SwitchFoldable :: "IRNode \<Rightarrow> bool" where
   "is_SwitchFoldable n = ((is_IfNode n))"
@@ -207,7 +210,7 @@ fun is_Binary :: "IRNode \<Rightarrow> bool" where
   "is_Binary n = ((is_BinaryArithmeticNode n) \<or> (is_BinaryNode n) \<or> (is_BinaryOpLogicNode n) \<or> (is_CompareNode n) \<or> (is_FixedBinaryNode n) \<or> (is_ShortCircuitOrNode n))"
 
 fun is_ArithmeticOperation :: "IRNode \<Rightarrow> bool" where
-  "is_ArithmeticOperation n = ((is_BinaryArithmeticNode n) \<or> (is_IntegerConvertNode n) \<or> (is_UnaryArithmeticNode n))"
+  "is_ArithmeticOperation n = ((is_BinaryArithmeticNode n) \<or> (is_IntegerConvertNode n) \<or> (is_ShiftNode n) \<or> (is_UnaryArithmeticNode n))"
 
 fun is_ValueNumberable :: "IRNode \<Rightarrow> bool" where
   "is_ValueNumberable n = ((is_FloatingNode n) \<or> (is_ProxyNode n))"

Graph/IRNodes.thy

@@ -56,6 +56,7 @@ datatype (discs_sels) IRNode =
   | InvokeWithExceptionNode (ir_nid: ID) (ir_callTarget: "INPUT_EXT") (ir_classInit_opt: "INPUT option") (ir_stateDuring_opt: "INPUT_STATE option") (ir_stateAfter_opt: "INPUT_STATE option") (ir_next: "SUCC") (ir_exceptionEdge: "SUCC") 
   | IsNullNode (ir_value: "INPUT") 
   | KillingBeginNode (ir_next: "SUCC") 
+  | LeftShiftNode (ir_x: "INPUT") (ir_y: "INPUT") 
   | LoadFieldNode (ir_nid: ID) (ir_field: string) (ir_object_opt: "INPUT option") (ir_next: "SUCC") 
   | LogicNegationNode (ir_value: "INPUT_COND") 
   | LoopBeginNode (ir_ends: "INPUT_ASSOC list") (ir_overflowGuard_opt: "INPUT_GUARD option") (ir_stateAfter_opt: "INPUT_STATE option") (ir_next: "SUCC") 
@@ -73,13 +74,15 @@ datatype (discs_sels) IRNode =
   | ParameterNode (ir_index: nat) 
   | PiNode (ir_object: "INPUT") (ir_guard_opt: "INPUT_GUARD option") 
   | ReturnNode (ir_result_opt: "INPUT option") (ir_memoryMap_opt: "INPUT_EXT option") 
+  | RightShiftNode (ir_x: "INPUT") (ir_y: "INPUT") 
   | ShortCircuitOrNode (ir_x: "INPUT_COND") (ir_y: "INPUT_COND") 
   | SignExtendNode (ir_inputBits: nat) (ir_resultBits: nat) (ir_value: "INPUT") 
   | SignedDivNode (ir_nid: ID) (ir_x: "INPUT") (ir_y: "INPUT") (ir_zeroCheck_opt: "INPUT_GUARD option") (ir_stateBefore_opt: "INPUT_STATE option") (ir_next: "SUCC") 
   | SignedRemNode (ir_nid: ID) (ir_x: "INPUT") (ir_y: "INPUT") (ir_zeroCheck_opt: "INPUT_GUARD option") (ir_stateBefore_opt: "INPUT_STATE option") (ir_next: "SUCC") 
   | StartNode (ir_stateAfter_opt: "INPUT_STATE option") (ir_next: "SUCC") 
   | StoreFieldNode (ir_nid: ID) (ir_field: string) (ir_value: "INPUT") (ir_stateAfter_opt: "INPUT_STATE option") (ir_object_opt: "INPUT option") (ir_next: "SUCC") 
   | SubNode (ir_x: "INPUT") (ir_y: "INPUT") 
+  | UnsignedRightShiftNode (ir_x: "INPUT") (ir_y: "INPUT") 
   | UnwindNode (ir_exception: "INPUT") 
   | ValuePhiNode (ir_nid: ID) (ir_values: "INPUT list") (ir_merge: "INPUT_ASSOC") 
   | ValueProxyNode (ir_value: "INPUT") (ir_loopExit: "INPUT_ASSOC") 
@@ -146,6 +149,8 @@ fun inputs_of :: "IRNode \<Rightarrow> ID list" where
   "inputs_of (IsNullNode value) = [value]" |
   inputs_of_KillingBeginNode:
   "inputs_of (KillingBeginNode next) = []" |
+  inputs_of_LeftShiftNode:
+  "inputs_of (LeftShiftNode x y) = [x, y]" |
   inputs_of_LoadFieldNode:
   "inputs_of (LoadFieldNode nid0 field object next) = (opt_to_list object)" |
   inputs_of_LogicNegationNode:
@@ -180,6 +185,8 @@ fun inputs_of :: "IRNode \<Rightarrow> ID list" where
   "inputs_of (PiNode object guard) = object # (opt_to_list guard)" |
   inputs_of_ReturnNode:
   "inputs_of (ReturnNode result memoryMap) = (opt_to_list result) @ (opt_to_list memoryMap)" |
+  inputs_of_RightShiftNode:
+  "inputs_of (RightShiftNode x y) = [x, y]" |
   inputs_of_ShortCircuitOrNode:
   "inputs_of (ShortCircuitOrNode x y) = [x, y]" |
   inputs_of_SignExtendNode:
@@ -194,6 +201,8 @@ fun inputs_of :: "IRNode \<Rightarrow> ID list" where
   "inputs_of (StoreFieldNode nid0 field value stateAfter object next) = value # (opt_to_list stateAfter) @ (opt_to_list object)" |
   inputs_of_SubNode:
   "inputs_of (SubNode x y) = [x, y]" |
+  inputs_of_UnsignedRightShiftNode:
+  "inputs_of (UnsignedRightShiftNode x y) = [x, y]" |
   inputs_of_UnwindNode:
   "inputs_of (UnwindNode exception) = [exception]" |
   inputs_of_ValuePhiNode:
@@ -249,6 +258,8 @@ fun successors_of :: "IRNode \<Rightarrow> ID list" where
   "successors_of (IsNullNode value) = []" |
   successors_of_KillingBeginNode:
   "successors_of (KillingBeginNode next) = [next]" |
+  successors_of_LeftShiftNode:
+  "successors_of (LeftShiftNode x y) = []" |
   successors_of_LoadFieldNode:
   "successors_of (LoadFieldNode nid0 field object next) = [next]" |
   successors_of_LogicNegationNode:
@@ -283,6 +294,8 @@ fun successors_of :: "IRNode \<Rightarrow> ID list" where
   "successors_of (PiNode object guard) = []" |
   successors_of_ReturnNode:
   "successors_of (ReturnNode result memoryMap) = []" |
+  successors_of_RightShiftNode:
+  "successors_of (RightShiftNode x y) = []" |
   successors_of_ShortCircuitOrNode:
   "successors_of (ShortCircuitOrNode x y) = []" |
   successors_of_SignExtendNode:
@@ -297,6 +310,8 @@ fun successors_of :: "IRNode \<Rightarrow> ID list" where
   "successors_of (StoreFieldNode nid0 field value stateAfter object next) = [next]" |
   successors_of_SubNode:
   "successors_of (SubNode x y) = []" |
+  successors_of_UnsignedRightShiftNode:
+  "successors_of (UnsignedRightShiftNode x y) = []" |
   successors_of_UnwindNode:
   "successors_of (UnwindNode exception) = []" |
   successors_of_ValuePhiNode:

Graph/Values.thy

@@ -235,6 +235,64 @@ fun intval_abs :: "Value \<Rightarrow> Value" where
   "intval_abs (IntVal64 v) = (if (v) <s 0 then (IntVal64 (- v)) else (IntVal64 v))" |
   "intval_abs _ = UndefVal"
 
+lemma [code]: "shiftl1 n = n * 2"
+  by (simp add: shiftl1_eq_mult_2)
+
+lemma [code]: "shiftr1 n = n div 2"
+  by (simp add: shiftr1_eq_div_2)
+
+lemma [code]: "sshiftr1 n = word_of_int (sint n div 2)"
+  using sshiftr1_eq by blast
+
+definition shiftl (infix "<<" 75) where 
+  "shiftl w n = (shiftl1 ^^ n) w"
+
+lemma shiftl_power[simp]: "(x::('a::len) word) * (2 ^ j) = x << j"
+  unfolding shiftl_def apply (induction j)
+  apply simp unfolding funpow_Suc_right
+  by (metis (no_types, lifting) comp_def funpow_swap1 mult.left_commute power_Suc shiftl1_eq_mult_2)
+
+lemma "(x::('a::len) word) * ((2 ^ j) + 1) = x << j + x"
+  by (simp add: distrib_left)
+
+lemma "(x::('a::len) word) * ((2 ^ j) - 1) = x << j - x"
+  by (simp add: right_diff_distrib)
+
+lemma "(x::('a::len) word) * ((2^j) + (2^k)) = x << j + x << k"
+  by (simp add: distrib_left)
+
+lemma "(x::('a::len) word) * ((2^j) - (2^k)) = x << j - x << k"
+  by (simp add: right_diff_distrib)
+
+
+definition signed_shiftr (infix ">>" 75) where 
+  "signed_shiftr w n = (sshiftr1 ^^ n) w"
+
+definition shiftr (infix ">>>" 75) where 
+  "shiftr w n = (shiftr1 ^^ n) w"
+
+lemma shiftr_power[simp]: "(x::('a::len) word) div (2 ^ j) = x >>> j"
+  unfolding shiftr_def apply (induction j)
+  apply simp unfolding funpow_Suc_right
+  by (metis (no_types, lifting) comp_apply div_exp_eq funpow_swap1 power_Suc2 power_add power_one_right shiftr1_eq_div_2)
+
+
+
+fun intval_left_shift :: "Value \<Rightarrow> Value \<Rightarrow> Value" where
+  "intval_left_shift (IntVal32 v1) (IntVal32 v2) = IntVal32 (v1 << unat (v2 mod 32))" |
+  "intval_left_shift (IntVal64 v1) (IntVal64 v2) = IntVal64 (v1 << unat (v2 mod 64))" |
+  "intval_left_shift _ _ = UndefVal"
+
+fun intval_right_shift :: "Value \<Rightarrow> Value \<Rightarrow> Value" where
+  "intval_right_shift (IntVal32 v1) (IntVal32 v2) = IntVal32 (v1 >> unat (v2 mod 32))" |
+  "intval_right_shift (IntVal64 v1) (IntVal64 v2) = IntVal64 (v1 >> unat (v2 mod 64))" |
+  "intval_right_shift _ _ = UndefVal"
+
+fun intval_uright_shift :: "Value \<Rightarrow> Value \<Rightarrow> Value" where
+  "intval_uright_shift (IntVal32 v1) (IntVal32 v2) = IntVal32 (v1 >>> unat (v2 mod 32))" |
+  "intval_uright_shift (IntVal64 v1) (IntVal64 v2) = IntVal64 (v1 >>> unat (v2 mod 64))" |
+  "intval_uright_shift _ _ = UndefVal"
+
 (*
 end
 *)

Optimizations/CanonicalizationTreeProofs.thy

@@ -790,7 +790,7 @@ next
       apply (cases "intval_equals xval yval")
       using IRTreeEval.val_to_bool.simps(2) apply presburger sorry
     then have "res = yval"
-      by (smt (verit) ConditionalExprE BinaryExprE xeval yeval evalDet bin_eval.simps(7) cond_eq.hyps(1) cond_eq.prems(1))
+      by (smt (verit, ccfv_threshold) BinaryExprE ConditionalExprE bin_eval.simps(10) cond_eq.hyps(1) cond_eq.prems(1) evalDet xeval yeval)
     then show ?thesis
       using cond_eq.prems(1) cond_eq.prems(2) xeval yeval evalDet by auto
   qed
@@ -803,8 +803,7 @@ next
   then show ?case proof (cases "val_to_bool(intval_less_than xval yval)")
     case True
     then show ?thesis
-      by (smt (verit, best) xeval yeval evalDet ConditionalExprE BinaryExprE bin_eval.simps(8)
-          condition_bounds_x.hyps(1) condition_bounds_x.prems(1) condition_bounds_x.prems(2))
+      by (smt (verit, best) BinaryExprE ConditionalExprE bin_eval.simps(11) condition_bounds_x.hyps(1) condition_bounds_x.prems(1) condition_bounds_x.prems(2) evalDet xeval yeval)
   next
     case False
     then have "stpi_upper stampx = stpi_lower stampy"
@@ -828,8 +827,7 @@ next
   then show ?case proof (cases "val_to_bool(intval_less_than xval yval)")
     case True
     then show ?thesis
-      by (smt (verit, best) xeval yeval evalDet ConditionalExprE BinaryExprE bin_eval.simps(8)
-          condition_bounds_y.hyps(1) condition_bounds_y.prems(1) condition_bounds_y.prems(2))
+      by (smt (verit, best) BinaryExprE ConditionalExprE bin_eval.simps(11) condition_bounds_y.hyps(1) condition_bounds_y.prems(1) condition_bounds_y.prems(2) evalDet xeval yeval)
   next
     case False
     have "stpi_upper stampx = stpi_lower stampy"

Semantics/IRTreeEval.thy

@@ -65,6 +65,9 @@ datatype IRBinaryOp =
   | BinAnd
   | BinOr
   | BinXor
+  | BinLeftShift
+  | BinRightShift
+  | BinURightShift
   | BinIntegerEquals
   | BinIntegerLessThan
   | BinIntegerBelow
@@ -121,6 +124,9 @@ fun bin_eval :: "IRBinaryOp \<Rightarrow> Value \<Rightarrow> Value \<Rightarrow
   "bin_eval BinAnd v1 v2 = intval_and v1 v2" |
   "bin_eval BinOr  v1 v2 = intval_or v1 v2" |
   "bin_eval BinXor v1 v2 = intval_xor v1 v2" |
+  "bin_eval BinLeftShift v1 v2 = intval_left_shift v1 v2" |
+  "bin_eval BinRightShift v1 v2 = intval_right_shift v1 v2" |
+  "bin_eval BinURightShift v1 v2 = intval_uright_shift v1 v2" |
   "bin_eval BinIntegerEquals v1 v2 = intval_equals v1 v2" |
   "bin_eval BinIntegerLessThan v1 v2 = intval_less_than v1 v2" |
   "bin_eval BinIntegerBelow v1 v2 = intval_below v1 v2"

Semantics/IRTreeEvalThms.thy

@@ -177,39 +177,39 @@ next
 next
   case (NotNode n x xe)
   then show ?case
-    by (metis IRNode.inject(31) NotNodeE rep_not)
+    by (metis IRNode.inject(32) NotNodeE rep_not)
 next
   case (NegateNode n x xe)
   then show ?case
-    by (metis  IRNode.inject(28) NegateNodeE rep_negate)
+    by (metis  IRNode.inject(29) NegateNodeE rep_negate)
 next
   case (LogicNegationNode n x xe)
   then show ?case
-    by (metis IRNode.inject(20) LogicNegationNodeE rep_logicnegation)
+    by (metis IRNode.inject(21) LogicNegationNodeE rep_logicnegation)
 next
   case (AddNode n x y xe ye)
   then show ?case
     by (metis AddNodeE IRNode.inject(2) rep_add) 
 next
   case (MulNode n x y xe ye)
   then show ?case
-    by (metis IRNode.inject(26) MulNodeE rep_mul)
+    by (metis IRNode.inject(27) MulNodeE rep_mul)
 next
   case (SubNode n x y xe ye)
   then show ?case
-    by (metis IRNode.inject(42) SubNodeE rep_sub)
+    by (metis IRNode.inject(44) SubNodeE rep_sub)
 next
   case (AndNode n x y xe ye)
   then show ?case
     by (metis AndNodeE IRNode.inject(3) rep_and)
 next
   case (OrNode n x y xe ye)
   then show ?case
-  by (metis IRNode.inject(32) OrNodeE rep_or)
+  by (metis IRNode.inject(33) OrNodeE rep_or)
 next
   case (XorNode n x y xe ye)
   then show ?case
-    by (metis IRNode.inject(46) XorNodeE rep_xor)
+    by (metis IRNode.inject(49) XorNodeE rep_xor)
 next
   case (IntegerBelowNode n x y xe ye)
   then show ?case
@@ -225,15 +225,15 @@ next
 next
   case (NarrowNode n x xe)
   then show ?case
-    by (metis IRNode.inject(27) NarrowNodeE rep_narrow)
+    by (metis IRNode.inject(28) NarrowNodeE rep_narrow)
 next
   case (SignExtendNode n x xe)
   then show ?case
-    by (metis IRNode.inject(37) SignExtendNodeE rep_sign_extend)
+    by (metis IRNode.inject(39) SignExtendNodeE rep_sign_extend)
 next
   case (ZeroExtendNode n x xe)
   then show ?case
-    by (metis IRNode.inject(47) ZeroExtendNodeE rep_zero_extend)
+    by (metis IRNode.inject(50) ZeroExtendNodeE rep_zero_extend)
 next
   case (LeafNode n s)
   then show ?case using rep_load_field LeafNodeE by blast 

Semantics/TreeToGraph.thy

@@ -283,6 +283,9 @@ fun bin_node :: "IRBinaryOp \<Rightarrow> ID \<Rightarrow> ID \<Rightarrow> IRNo
   "bin_node BinAnd x y = AndNode x y" |
   "bin_node BinOr  x y = OrNode x y" |
   "bin_node BinXor x y = XorNode x y" |
+  "bin_node BinLeftShift x y = LeftShiftNode x y" |
+  "bin_node BinRightShift x y = RightShiftNode x y" |
+  "bin_node BinURightShift x y = UnsignedRightShiftNode x y" |
   "bin_node BinIntegerEquals x y = IntegerEqualsNode x y" |
   "bin_node BinIntegerLessThan x y = IntegerLessThanNode x y" |
   "bin_node BinIntegerBelow x y = IntegerBelowNode x y"

TheoryTesting.thy

@@ -44,6 +44,40 @@ lemma
   using assms unfolding valid_number.simps
   apply (simp add: Abs_IntegerHole_inverse)
   by (metis (no_types, hide_lams) bit.conj_disj_distrib2 bit.disj_cancel_left or.left_neutral word_ao_absorbs(2) word_oa_dist)
-  
+
+
+definition shiftl (infix "<<" 75) where 
+  "shiftl w n = (shiftl1 ^^ n) w"
+
+lemma shiftl_power[simp]: "(x::('a::len) word) * (2 ^ j) = x << j"
+  unfolding shiftl_def apply (induction j)
+  apply simp unfolding funpow_Suc_right
+  by (metis (no_types, lifting) comp_def funpow_swap1 mult.left_commute power_Suc shiftl1_eq_mult_2)
+
+lemma "(x::('a::len) word) * ((2 ^ j) + 1) = x << j + x"
+  by (simp add: distrib_left)
+
+lemma "(x::('a::len) word) * ((2 ^ j) - 1) = x << j - x"
+  by (simp add: right_diff_distrib)
+
+lemma "(x::('a::len) word) * ((2^j) + (2^k)) = x << j + x << k"
+  by (simp add: distrib_left)
+
+lemma "(x::('a::len) word) * ((2^j) - (2^k)) = x << j - x << k"
+  by (simp add: right_diff_distrib)
+
+
+definition signed_shiftr (infix ">>" 75) where 
+  "signed_shiftr w n = (sshiftr1 ^^ n) w"
+
+definition shiftr (infix ">>>" 75) where 
+  "shiftr w n = (shiftr1 ^^ n) w"
+
+lemma shiftr_power[simp]: "(x::('a::len) word) div (2 ^ j) = x >>> j"
+  unfolding shiftr_def apply (induction j)
+  apply simp unfolding funpow_Suc_right
+  by (metis (no_types, lifting) comp_apply div_exp_eq funpow_swap1 power_Suc2 power_add power_one_right shiftr1_eq_div_2)
+
+
 
 end