Take into account witnesses when computing [lessequal] on values

backend/checkmach.ml

@@ -88,6 +88,8 @@ module Witnesses : sig
 
   val meet : t -> t -> t
 
+  val lessequal : t -> t -> bool
+
   val create : Witness.kind -> Debuginfo.t -> t
 
   val print : Format.formatter -> t -> unit
@@ -113,6 +115,8 @@ end = struct
 
   let meet = inter
 
+  let lessequal = subset
+
   let create kind dbg = singleton (Witness.create dbg kind)
 
   let iter t ~f = iter f t
@@ -167,11 +171,15 @@ end = struct
     match t with Top w -> w | Bot | Safe -> Witnesses.empty
 
   let diff_witnesses ~expected ~actual =
-    if lessequal actual expected
-    then Witnesses.empty
-    else (
-      assert (expected = Safe);
-      match actual with Bot | Safe -> assert false | Top w -> w)
+    (* If [actual] is Top and [expected] is not Top then return the [actual]
+       witnesses. Otherwise, return empty. *)
+    match actual, expected with
+    | Bot, Bot | Safe, Safe | Bot, Safe -> Witnesses.empty
+    | Bot, Top w | Safe, Top w | Top _, Top w ->
+      assert (Witnesses.is_empty w);
+      Witnesses.empty
+    | Safe, Bot -> Witnesses.empty
+    | Top w, (Bot | Safe) -> w
 end
 
 module Value : sig
@@ -221,7 +229,14 @@ module Annotation : sig
   val find :
     Cmm.codegen_option list -> Cmm.property -> string -> Debuginfo.t -> t option
 
-  val expected_value : t -> Witnesses.t -> Value.t
+  val expected_value : t -> Value.t
+
+  (** [valid t value] returns true if and only if the [value] satisfies the annotation,
+      i.e., [value] is less or equal to [expected_value a] when ignoring witnesses. *)
+
+  val valid : t -> Value.t -> bool
+
+  val diff_witnesses : t -> Value.t -> Witnesses.components
 
   val is_assume : t -> bool
 
@@ -257,13 +272,23 @@ end = struct
 
   let get_loc t = t.loc
 
-  let expected_value t w =
-    let res = if t.strict then Value.safe else Value.relaxed w in
+  let expected_value t =
+    let res = if t.strict then Value.safe else Value.relaxed Witnesses.empty in
     let res =
       if t.never_returns_normally then { res with nor = V.Bot } else res
     in
     res
 
+  let valid t v =
+    (* Use Value.lessequal but ignore witnesses. *)
+    let expected = expected_value t in
+    let actual = Value.replace_witnesses Witnesses.empty v in
+    Value.lessequal actual expected
+
+  let diff_witnesses t v =
+    let expected = expected_value t in
+    Value.diff_witnesses ~actual:v ~expected
+
   let is_assume t = t.assume
 
   let is_strict t = t.strict
@@ -696,10 +721,9 @@ end = struct
       | Some a ->
         Builtin_attributes.mark_property_checked analysis_name
           (Annotation.get_loc a);
-        let expected_value = Annotation.expected_value a Witnesses.empty in
         if (not (Annotation.is_assume a))
            && S.enabled ()
-           && not (Value.lessequal func_info.value expected_value)
+           && not (Annotation.valid a func_info.value)
         then
           (* CR-soon gyorsh: keeping track of all the witnesses until the end of
              the compilation unit will be expensive. For functions that do not
@@ -710,10 +734,7 @@ end = struct
           (* CR gyorsh: we can add error recovering mode where we sets the
              expected value as the actual value and continue analysis of other
              functions. *)
-          let witnesses =
-            Value.diff_witnesses ~expected:expected_value
-              ~actual:func_info.value
-          in
+          let witnesses = Annotation.diff_witnesses a func_info.value in
           errors
             := { Report.a;
                  fun_name = func_info.name;
@@ -1036,12 +1057,12 @@ end = struct
       in
       match a with
       | Some a when Annotation.is_assume a ->
-        let expected_value = Annotation.expected_value a Witnesses.empty in
+        let expected_value = Annotation.expected_value a in
         report t expected_value ~msg:"assumed" ~desc:"fundecl" f.fun_dbg;
         Unit_info.record unit_info fun_name expected_value f.fun_dbg None None
       | None -> really_check ()
       | Some a ->
-        let expected_value = Annotation.expected_value a Witnesses.empty in
+        let expected_value = Annotation.expected_value a in
         report t expected_value ~msg:"assert" ~desc:"fundecl" f.fun_dbg;
         (* Only keep witnesses for functions that need checking. *)
         really_check ()

ocaml/lambda/assume_info.ml

@@ -34,6 +34,7 @@ module Witnesses = struct
   type t = unit
 
   let join _ _ = ()
+  let lessequal _ _ = true
   let meet _ _ = ()
   let print _ _ = ()
   let empty = ()

ocaml/lambda/assume_info.mli

@@ -15,6 +15,7 @@ module Witnesses : sig
 
   val join : t -> t -> t
   val meet : t -> t -> t
+  val lessequal : t -> t -> bool
   val print : Format.formatter -> t -> unit
   val compare : t -> t -> int
 end

ocaml/utils/zero_alloc_utils.ml

@@ -5,6 +5,8 @@ module type WS = sig
 
   val meet : t -> t -> t
 
+  val lessequal : t -> t -> bool
+
   val print : Format.formatter -> t -> unit
 
   val compare : t -> t -> int
@@ -39,7 +41,7 @@ module Make (Witnesses : WS) = struct
       match v1, v2 with
       | Bot, Bot -> true
       | Safe, Safe -> true
-      | Top _, Top _ -> true
+      | Top w1, Top w2 -> Witnesses.lessequal w1 w2
       | Bot, Safe -> true
       | Bot, Top _ -> true
       | Safe, Top _ -> true

ocaml/utils/zero_alloc_utils.mli

@@ -10,6 +10,8 @@ module type WS = sig
 
   val meet : t -> t -> t
 
+  val lessequal : t -> t -> bool
+
   val print : Format.formatter -> t -> unit
 
   val compare : t -> t -> int