Support wildcard for fractional permissions in WISL

transformers/lib/prebuilt/WISLF.ml

@@ -1,14 +1,15 @@
 open Utils
 open Gil_syntax
 module Delayed = Gillian.Monadic.Delayed
+module Frac_used = Fractional.Frac_with_wildcard
 
 (* Make the default value null *)
 module FractionalNull = struct
-  include Fractional
+  include Fractional.Make (Frac_used)
 
   let instantiate = function
-    | [] -> (Some (Expr.Lit Null, Expr.num 1.0), [])
-    | [ v ] -> (Some (v, Expr.num 1.0), [])
+    | [] -> (Some (Expr.Lit Null, Frac_used._1), [])
+    | [ v ] -> (Some (v, Frac_used._1), [])
     | _ -> failwith "FractionalNull: instantiate: too many arguments"
 end
 

transformers/lib/states/Fractional.ml

@@ -5,119 +5,201 @@ open Gil_syntax
 module DR = Delayed_result
 module Recovery_tactic = Gillian.General.Recovery_tactic
 
-let _0 = Expr.num 0.
-let _1 = Expr.num 1.
-
-(** Value * Fraction *)
-type t = (Expr.t * Expr.t) option [@@deriving show, yojson]
-
-type err_t = MissingState | NotEnoughPermission [@@deriving show, yojson]
-type action = Load | Store
-type pred = Frac
-
-let action_from_str = function
-  | "load" -> Some Load
-  | "store" -> Some Store
-  | _ -> None
-
-let action_to_str = function
-  | Load -> "load"
-  | Store -> "store"
-
-let list_actions () = [ (Load, [], [ "value" ]); (Store, [ "value" ], []) ]
-
-let pred_from_str = function
-  | "frac" -> Some Frac
-  | _ -> None
-
-let pred_to_str = function
-  | Frac -> "frac"
-
-let list_preds () = [ (Frac, [ "fraction" ], [ "value" ]) ]
-let empty () : t = None
-
-let[@inline] execute_action action s args =
-  let open Expr.Infix in
-  match (action, s, args) with
-  | _, None, _ -> DR.error MissingState
-  | Load, Some (v, q), [] -> DR.ok (Some (v, q), [ v ])
-  | Store, Some (_, q), [ v' ] ->
-      if%sat q == _1 then DR.ok (Some (v', q), [])
+type err = MissingState | NotEnoughPermission [@@deriving show, yojson]
+
+module type FracA_S = sig
+  type t [@@deriving yojson, show]
+
+  val of_expr : Expr.t -> t
+  val to_expr : t -> Expr.t
+  val subst : Values.et -> t -> t
+  val subtract : t -> t -> (t option, err) result Delayed.t
+  val add : t -> t -> t Delayed.t
+  val _1 : t
+  val is_1 : t -> Expr.t
+  val is_concrete : t -> bool
+end
+
+module Classic_fracA = struct
+  let _0 = Expr.num 0.
+  let _1 = Expr.num 1.
+
+  type t = Expr.t [@@deriving show, yojson]
+
+  let is_concrete = Expr.is_concrete
+  let of_expr x = x
+  let to_expr x = x
+  let subst s = Subst.subst_in_expr s ~partial:true
+
+  open Expr.Infix
+
+  let subtract left right =
+    if%sat left == right then DR.ok None
+    else
+      if%sat left >=. right then DR.ok (Some (left -. right))
       else DR.error NotEnoughPermission
-  | a, _, args ->
-      Fmt.failwith "Invalid action %s with state %a and args %a"
-        (action_to_str a) pp s (Fmt.Dump.list Expr.pp) args
-
-let[@inline] consume core_pred s args =
-  let open Expr.Infix in
-  match (core_pred, s, args) with
-  | Frac, Some (v, q), [ q' ] ->
-      if%sat q == q' then DR.ok (None, [ v ])
-      else
-        if%sat q >=. q' then
-          DR.ok ~learned:[ q' >. _0 ] (Some (v, q -. q'), [ v ])
+
+  let add left right =
+    Delayed.return ~learned:[ left +. right <=. _1 ] (left +. right)
+
+  let is_1 q = q == _1
+end
+
+module Frac_with_wildcard : FracA_S = struct
+  type t = Q of Expr.t | Wildcard [@@deriving show, yojson]
+
+  let _1 = Q (Expr.num 1.)
+
+  let is_concrete = function
+    | Wildcard -> false
+    | Q q -> Expr.is_concrete q
+
+  let of_expr = function
+    | Expr.Lit (String "_") -> Wildcard
+    | x -> Q x
+
+  let to_expr = function
+    | Wildcard -> Expr.Lit (String "_")
+    | Q q -> q
+
+  let subst s = function
+    | Wildcard -> Wildcard
+    | Q q -> Q (Classic_fracA.subst s q)
+
+  let subtract left right =
+    let open DR.Syntax in
+    match (left, right) with
+    | Wildcard, Wildcard -> DR.ok None
+    | Wildcard, Q _ | Q _, Wildcard -> DR.error NotEnoughPermission
+    | Q left, Q right ->
+        let++ q = Classic_fracA.subtract left right in
+        Option.map (fun q -> Q q) q
+
+  let add left right =
+    let open Delayed.Syntax in
+    match (left, right) with
+    (* Note: the following is over-approximating, because two wildcard could get bigger than 1. *)
+    | Wildcard, _ | _, Wildcard -> Delayed.return Wildcard
+    | Q x, Q y ->
+        let+ r = Classic_fracA.add x y in
+        Q r
+
+  let is_1 = function
+    | Wildcard -> Expr.false_
+    | Q q -> Classic_fracA.is_1 q
+end
+
+module Make (FracA : FracA_S) = struct
+  (** Value * Fraction *)
+  type t = (Expr.t * FracA.t) option [@@deriving show, yojson]
+
+  type err_t = err [@@deriving show, yojson]
+  type action = Load | Store
+  type pred = Frac
+
+  let action_from_str = function
+    | "load" -> Some Load
+    | "store" -> Some Store
+    | _ -> None
+
+  let action_to_str = function
+    | Load -> "load"
+    | Store -> "store"
+
+  let list_actions () = [ (Load, [], [ "value" ]); (Store, [ "value" ], []) ]
+
+  let pred_from_str = function
+    | "frac" -> Some Frac
+    | _ -> None
+
+  let pred_to_str = function
+    | Frac -> "frac"
+
+  let list_preds () = [ (Frac, [ "fraction" ], [ "value" ]) ]
+  let empty () : t = None
+
+  let[@inline] execute_action action (s : t) args =
+    match (action, s, args) with
+    | _, None, _ -> DR.error MissingState
+    | Load, Some (v, q), [] -> DR.ok (Some (v, q), [ v ])
+    | Store, Some (_, q), [ v' ] ->
+        if%sat FracA.is_1 q then DR.ok (Some (v', q), [])
         else DR.error NotEnoughPermission
-  | Frac, None, _ -> DR.error MissingState
-  | Frac, _, _ -> failwith "Invalid Agree consume"
-
-let[@inline] produce core_pred s args =
-  let open Expr.Infix in
-  match (core_pred, s, args) with
-  | Frac, None, [ q'; v' ] -> Delayed.return (Some (v', q'))
-  | Frac, Some (v, q), [ q'; v' ] ->
-      Delayed.return ~learned:[ v == v'; q +. q' <=. _1 ] (Some (v, q +. q'))
-  | Frac, _, _ -> failwith "Invalid Frac produce"
-
-let substitution_in_place subst s =
-  match s with
-  | None -> Delayed.return None
-  | Some (v, q) ->
-      let v' = Subst.subst_in_expr ~partial:true subst v in
-      let q' = Subst.subst_in_expr ~partial:true subst q in
-      Delayed.return (Some (v', q'))
-
-let compose (s1 : t) (s2 : t) =
-  let open Expr.Infix in
-  match (s1, s2) with
-  | None, _ -> Delayed.return s2
-  | _, None -> Delayed.return s1
-  | Some (v, q), Some (v', q') ->
-      Delayed.return ~learned:[ v == v'; q +. q' <=. _1 ] (Some (v, q +. q'))
-
-let is_exclusively_owned s _ =
-  match s with
-  | None -> Delayed.return false
-  | Some (_, q) -> Delayed.check_sat Expr.Infix.(q == _1)
-
-let is_empty = function
-  | None -> true
-  | Some _ -> false
-
-let is_concrete = function
-  | None -> true
-  | Some (v, q) -> Expr.is_concrete v && Expr.is_concrete q
-
-let instantiate = function
-  | [] -> (Some (Expr.int 0, _1), [])
-  | _ -> failwith "Invalid Fractional instantiation"
-
-let lvars = function
-  | None -> Containers.SS.empty
-  | Some (v, _) -> Expr.lvars v
-
-let alocs = function
-  | None -> Containers.SS.empty
-  | Some (v, _) -> Expr.alocs v
-
-let assertions = function
-  | None -> []
-  | Some (v, q) -> [ (Frac, [ q ], [ v ]) ]
-
-let assertions_others _ = []
-let get_recovery_tactic _ = Recovery_tactic.none
-
-let can_fix = function
-  | _ -> false
-
-let get_fixes = function
-  | _ -> []
+    | a, _, args ->
+        Fmt.failwith "Invalid action %s with state %a and args %a"
+          (action_to_str a) pp s (Fmt.Dump.list Expr.pp) args
+
+  let consume core_pred s args =
+    let open Expr.Infix in
+    match (core_pred, s, args) with
+    | Frac, Some (v, q), [ q' ] ->
+        if%sat q == q' then DR.ok (None, [ v ])
+        else
+          DR.ok ~learned:[ q' >. _0; q -. q' >. _0 ] (Some (v, q -. q'), [ v ])
+    | Frac, None, _ -> DR.error MissingState
+    | Frac, _, _ -> failwith "Invalid Agree consume"
+
+  let produce core_pred s args =
+    let open Expr.Infix in
+    match (core_pred, s, args) with
+    | Frac, None, [ q'; v' ] -> Delayed.return (Some (v', q'))
+    | Frac, Some (v, q), [ q'; v' ] ->
+        Delayed.return ~learned:[ v == v'; q +. q' <=. _1 ] (Some (v, q +. q'))
+    | Frac, _, _ -> failwith "Invalid Frac produce"
+
+  let substitution_in_place subst s =
+    match s with
+    | None -> Delayed.return None
+    | Some (v, q) ->
+        let v' = Subst.subst_in_expr ~partial:true subst v in
+        let q' = FracA.subst subst q in
+        Delayed.return (Some (v', q'))
+
+  let compose (s1 : t) (s2 : t) =
+    let open Expr.Infix in
+    let open Delayed.Syntax in
+    match (s1, s2) with
+    | None, _ -> Delayed.return s2
+    | _, None -> Delayed.return s1
+    | Some (v, q), Some (v', q') ->
+        let* new_q = FracA.add q q' in
+        Delayed.return ~learned:[ v == v' ] (Some (v, new_q))
+
+  let is_exclusively_owned s _ =
+    match s with
+    | None -> Delayed.return false
+    | Some (_, q) -> Delayed.check_sat (FracA.is_1 q)
+
+  let is_empty = function
+    | None -> true
+    | Some _ -> false
+
+  let is_concrete = function
+    | None -> true
+    | Some (v, q) -> Expr.is_concrete v && FracA.is_concrete q
+
+  let instantiate : 'a list -> t * Expr.t list = function
+    | [] -> (Some (Expr.int 0, FracA._1), [])
+    | _ -> failwith "Invalid Fractional instantiation"
+
+  let lvars = function
+    | None -> Containers.SS.empty
+    | Some (v, _) -> Expr.lvars v
+
+  let alocs = function
+    | None -> Containers.SS.empty
+    | Some (v, _) -> Expr.alocs v
+
+  let assertions = function
+    | None -> []
+    | Some (v, q) -> [ (Frac, [ FracA.to_expr q ], [ v ]) ]
+
+  let assertions_others _ = []
+  let get_recovery_tactic _ _ = Recovery_tactic.none
+
+  let can_fix = function
+    | _ -> false
+
+  let get_fixes = function
+    | _ -> []
+end

wisl/examples/frac/wildcard.wisl

@@ -0,0 +1,63 @@
+// Successfully verifies
+{ (x == #x) * (#x -> ("_" : #a)) }
+function wildcard_consumes_wildcard(x) {
+    r := [x];
+    return r
+}
+{ (#x -> ("_" : #a)) * (ret == #a) }
+
+
+// Fails to match against post-condition
+{ (x == #x) * (#x -> (0.5 : #a)) }
+function cannot_consume_wildcard_from_value(x) {
+    r := [x];
+    return r
+}
+{ (#x -> ("_" : #a)) * (ret == #a) }
+
+// Fails to match against post-condition
+{ (x == #x) * (#x -> ("_" : #a)) }
+function cannot_consume_value_from_wildcard(x) {
+    r := [x];
+    return r
+}
+{ (#x -> (0.5 : #a)) * (ret == #a) }
+
+// Successfully verifies
+{ (x == #x) * (#x -> ("_" : #a)) * (#x -> (0.5 : #a)) }
+function value_plus_wildcard_is_wildcard(x) {
+    // Current symbolic heap has wildcard permission for #x
+    r := [x];
+    return r
+}
+{ (#x -> ("_" : #a)) * (ret == #a) }
+
+// Successfully verifies
+{ (x == #x) * (#x -> ("_" : #a)) }
+function cannot_write_wildcard(x) {
+    [x] := 0;
+    return 0
+}
+{ (#x -> ("_" : 0)) * (ret == 0) }
+
+// t_wislf verify wisl/examples/frac/wildcard.wisl -l tmi
+//
+// Parsing and compiling...                 
+// Preprocessing...
+// Obtaining specs to verify...
+// Obtaining lemmas to verify...
+// Obtained 5 symbolic tests in total
+// Running symbolic tests: 0.009271
+// Verifying one spec of procedure value_plus_wildcard_is_wildcard... s Success
+// Verifying one spec of procedure wildcard_consumes_wildcard... s Success
+// Verifying one spec of procedure cannot_consume_wildcard_from_value... f Failure
+// Verifying one spec of procedure cannot_consume_value_from_wildcard... f Failure
+// Verifying one spec of procedure cannot_write_wildcard... f Failure
+// There were failures: 0.013057
+// Analysis failures!
+// 1. Couldn't satisfy postcondition [wisl/examples/frac/wildcard.wisl 16:3-35]
+// 2. Couldn't satisfy postcondition [wisl/examples/frac/wildcard.wisl 24:3-35]
+// 3. (PMap.MakeOpen.SubError (#loc_4, #loc_4,
+//    (Freeable.Make.SubError
+//       (MList.Make.SubError (#wisl__1, Fractional.NotEnoughPermission))) <--- Not enough permission to write
+//    )) [wisl/examples/frac/wildcard.wisl 38:5-13]