[herd] Add is_zero function

lib/ASLScalar.ml

@@ -106,6 +106,12 @@ let to_int64 = function
   | S_BitVector bv -> BV.to_int64_signed bv
   | S_Label _ -> Warn.fatal "Trying to convert a label to int"
 
+let is_zero = function
+  | S_Bool b -> not b (* Zero for BAnd/BOr ... *)
+  | S_Int z -> Z.equal Z.zero z
+  | S_BitVector bv -> BV.is_zeros bv
+  | S_Label _ -> false
+
 let as_bool = function
   | S_Bool b -> Some b
   | _ -> None

lib/SVEScalar.ml

@@ -30,7 +30,6 @@ module BV = struct
   let compare = Z.compare
   let equal = Z.equal
 
-
   let logor = Z.logor
   and logand = Z.logand
   and logxor = Z.logxor
@@ -56,6 +55,8 @@ module BV = struct
     | Word -> fun v ->  Z.logand v mask32
     | Quad -> fun v -> logand v mask64
     | S128 -> Misc.identity
+
+  let is_zero = Z.equal Z.zero
 end
 
 module Translate = struct

lib/capabilityScalar.ml

@@ -101,7 +101,8 @@ let sxt sz v = match sz with
      let m = Uint128.shift_left Uint128.one (nb-1) in
      t,Uint128.sub (Uint128.logxor v m) m
 
-let as_bool (_, v) = Some (Bool.not (Uint128.equal Uint128.zero v))
+let is_zero (_, v) = Uint128.equal Uint128.zero v
+let as_bool s = Some (Bool.not (is_zero s))
 let s_true = one
 let s_false = zero
 

lib/constant.ml

@@ -494,4 +494,5 @@ module type S =  sig
   val eq : v -> v -> bool
   val vToName : v -> string
   val is_nop : v -> bool
+  val is_zero : v -> bool
 end

lib/constant.mli

@@ -186,5 +186,5 @@ module type S =  sig
   val eq : v -> v -> bool
   val vToName : v -> string
   val is_nop : v -> bool
-
+  val is_zero : v -> bool
 end

lib/extendScalar.ml

@@ -65,6 +65,7 @@ module
       | Narrow i -> Narrow.as_bool i
       | Wide i -> Warn.fatal "as_bool on wide scalar '%s'" @@ Wide.pp i
 
+    let is_zero = choose Narrow.is_zero Wide.is_zero
     let printable = map Narrow.printable Misc.identity
 
     let compare s1 s2 = match s1,s2 with

lib/int128Scalar.ml

@@ -78,7 +78,8 @@ let zero = Int128.zero
 type t = Int128.t
 let unsigned_compare = Int128.unsigned_compare
 
-let as_bool v = Some (Bool.not (Int128.equal Int128.zero v))
+let is_zero v = Int128.equal Int128.zero v
+let as_bool v = Some (Bool.not (is_zero v))
 let s_true = one
 let s_false = zero
 

lib/int32Scalar.ml

@@ -59,7 +59,8 @@ let sxt sz v =
      let m = shift_left one (nb-1) in
      sub (logxor v m) m
 
-let as_bool v = Some (Bool.not (Int32.equal Int32.zero v))
+let is_zero v = Int32.equal Int32.zero v
+let as_bool v = Some (Bool.not (is_zero v))
 let s_true = one
 let s_false = zero
 

lib/int64Scalar.ml

@@ -61,7 +61,8 @@ let sxt sz v =
 let of_int64 = Misc.identity
 let to_int64 = Misc.identity
 
-let as_bool v = Some (Bool.not (Int64.equal Int64.zero v))
+let is_zero = Int64.equal Int64.zero
+let as_bool v = Some (Bool.not (is_zero v))
 let s_true = one
 let s_false = zero
 

lib/scalar.mli

@@ -41,6 +41,9 @@ module type S = sig
 
   val as_bool : t -> bool option
 
+  (** [is_zero s] is true if and only if [s] is identity wrt [add]/[sub]. *)
+  val is_zero : t -> bool
+
   val printable : t -> t
   val compare : t -> t -> int
   val unsigned_compare : t -> t -> int

lib/symbConstant.ml

@@ -51,6 +51,10 @@ module Make
     | Concrete c -> Scalar.as_bool c
     | _ -> None
 
+  let is_zero = function
+    | Concrete c -> Scalar.is_zero c
+    | _ -> false
+
   let pp_instr_cst i = Instr.pp i
 
   let pp hexa =

lib/symbValue.ml

@@ -137,7 +137,7 @@ module
   exception Undetermined
 
   let is_zero v = match v with
-  | Val cst -> Cst.eq cst Cst.zero
+  | Val cst -> Cst.is_zero cst
   | Var _ -> raise  Undetermined
 
   let is_one v = match v with
@@ -454,8 +454,8 @@ module
 
   let lt v1 v2 = match v1,v2 with
 (* Need to compare symbols to zero, for setting X86_64 flags *)
-    | Val (Symbolic _),Val c when Cst.eq c Cst.zero -> zero
-    | Val c,Val (Symbolic _) when Cst.eq c Cst.zero -> one
+    | Val (Symbolic _),Val c when Cst.is_zero c -> zero
+    | Val c,Val (Symbolic _) when Cst.is_zero c -> one
     | _,_ ->
        binop Op.Lt
          (fun s1 s2 -> bool_to_scalar (Cst.Scalar.lt s1 s2)) v1 v2
@@ -590,7 +590,7 @@ module
   | Val c -> Constant.as_virtual c
   | Var _ -> raise Undetermined
 
-  let is_virtual_v v =  if is_virtual v then one else zero
+  let is_virtual_v v = if is_virtual v then v_true else v_false
 
   let is_instrloc v = match v with
   | Val c -> Constant.is_label c
@@ -846,10 +846,7 @@ module
     | ReadBit k ->
         (* ReadBit returns 0 or 1, not false or true *)
         unop op
-          (fun s ->
-             if equal (logand (mask_one k) s) zero
-             then zero
-             else one)
+          (fun s -> if is_zero (logand (mask_one k) s) then zero else one)
     | LogicalRightShift 0
     | LeftShift 0
     | AddK 0 -> fun s -> s

lib/uint128Scalar.ml

@@ -59,7 +59,8 @@ let sxt sz v = match sz with
      let m = Uint128.shift_left Uint128.one (nb-1) in
      Uint128.sub (Uint128.logxor v m) m
 
-let as_bool v = Some (Bool.not (Uint128.equal Uint128.zero v))
+let is_zero = Uint128.equal Uint128.zero
+let as_bool v = Some (Bool.not (is_zero v))
 let s_true = one
 let s_false = zero
 

lib/wideScalar.mli

@@ -57,4 +57,6 @@ module type S = sig
   val lt : t -> t -> bool
   val le : t -> t -> bool
   val mask : MachSize.sz -> t -> t
+
+  val is_zero : t -> bool
 end