From a9bd91c6bad2bac375833c23bb3011019287a713 Mon Sep 17 00:00:00 2001 From: Hadrien Renaud Date: Thu, 30 Jan 2025 11:24:03 +0000 Subject: [PATCH] [asl] Re-implement approximations of constraints --- asllib/Typing.ml | 3 +- asllib/diet.ml | 43 ++++++-- asllib/diet.mli | 28 +++++- asllib/types.ml | 253 +++++++++++++++++++---------------------------- 4 files changed, 164 insertions(+), 163 deletions(-) diff --git a/asllib/Typing.ml b/asllib/Typing.ml index 4f3f438ef..bc49be282 100644 --- a/asllib/Typing.ml +++ b/asllib/Typing.ml @@ -760,8 +760,7 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct (* Begin CheckPositionsInWidth *) let check_diet_in_width ~loc slices width diet () = - let min_pos = Diet.Int.min_elt diet |> Diet.Int.Interval.x - and max_pos = Diet.Int.max_elt diet |> Diet.Int.Interval.y in + let min_pos = Diet.Int.min_elt diet and max_pos = Diet.Int.max_elt diet in if 0 <= min_pos && max_pos < width then () |: TypingRule.CheckPositionsInWidth else fatal_from ~loc (BadSlices (Error.Static, slices, width)) diff --git a/asllib/diet.ml b/asllib/diet.ml index fd9512bf7..a70033c37 100644 --- a/asllib/diet.ml +++ b/asllib/diet.ml @@ -54,14 +54,20 @@ module type INTERVAL_SET = sig val iter : (interval -> unit) -> t -> unit val add : interval -> t -> t val remove : interval -> t -> t - val min_elt : t -> interval - val max_elt : t -> interval + val min_elt : t -> elt + val max_elt : t -> elt + val min_interval : t -> interval + val max_interval : t -> interval val choose : t -> interval val take : t -> elt -> (t * t) option val union : t -> t -> t val diff : t -> t -> t val inter : t -> t -> t + val subset : t -> t -> bool val find_next_gap : elt -> t -> elt + val elements : t -> interval list + val elements_individual : t -> elt list + val of_list : elt list -> t val check_invariants : t -> (unit, string) result val height : t -> int end @@ -246,16 +252,18 @@ module Make (Elt : ELT) = struct (* or search left or search right *) if elt < n.x then mem elt n.l else mem elt n.r - let rec min_elt = function + let rec min_interval = function | Empty -> raise Not_found | Node { x; y; l = Empty; _ } -> (x, y) - | Node { l; _ } -> min_elt l + | Node { l; _ } -> min_interval l - let rec max_elt = function + let rec max_interval = function | Empty -> raise Not_found | Node { x; y; r = Empty; _ } -> (x, y) - | Node { r; _ } -> max_elt r + | Node { r; _ } -> max_interval r + let min_elt t = min_interval t |> Interval.x + let max_elt t = max_interval t |> Interval.y let choose = function Empty -> raise Not_found | Node { x; y; _ } -> (x, y) (* fold over the maximal contiguous intervals *) @@ -277,6 +285,9 @@ module Make (Elt : ELT) = struct in fold range t acc + let elements t = fold List.cons t [] + let elements_individual t = fold_individual List.cons t [] + (* iterate over maximal contiguous intervals *) let iter f t = let f' itl () = f itl in @@ -393,6 +404,7 @@ module Make (Elt : ELT) = struct let diff a b = fold remove b a let inter a b = diff a (diff a b) + let subset a b = is_empty (diff a b) let rec find_next_gap from = function | Empty -> from @@ -421,6 +433,23 @@ module Make (Elt : ELT) = struct in loop empty t n + let _make_intervals = + let rec loop acc ((x, y) as i) = function + | [] -> List.map (fun (a, b) -> Interval.make a b) (i :: acc) + | z :: t -> + let y' = Elt.succ y in + if eq y' z then loop acc (x, y') t + else ( + assert (y' < z); + loop (i :: acc) (z, z) t) + in + function [] -> [] | x :: t -> loop [] (x, x) t + + let of_list li = + List.sort_uniq Elt.compare li + |> _make_intervals + |> List.fold_left (fun acc elt -> add elt acc) empty + let check_invariants = Invariant.check let singleton x = add (Interval.make x x) empty @@ -434,7 +463,7 @@ module Make (Elt : ELT) = struct function | Empty -> fprintf fmt "∅" | t -> - let m = min_elt t in + let m = min_interval t in let t = remove m t in pp_open_hovbox fmt 0; pp_interval fmt m; diff --git a/asllib/diet.mli b/asllib/diet.mli index c3afe4bee..bd20c1fb9 100644 --- a/asllib/diet.mli +++ b/asllib/diet.mli @@ -104,12 +104,20 @@ module type INTERVAL_SET = sig val remove : interval -> t -> t (** [remove interval t] returns the set consisting of [t] minus [interval] *) - val min_elt : t -> interval - (** [min_elt t] returns the smallest (in terms of the ordering) interval in + val min_elt : t -> elt + (** [min_elt t] returns the smallest (in terms of the ordering) element in [t], or raises [Not_found] if the set is empty. *) - val max_elt : t -> interval - (** [max_elt t] returns the largest (in terms of the ordering) interval in + val max_elt : t -> elt + (** [max_elt t] returns the largest (in terms of the ordering) element in + [t], or raises [Not_found] if the set is empty. *) + + val min_interval : t -> interval + (** [min_interval t] returns the smallest (in terms of the ordering) interval in + [t], or raises [Not_found] if the set is empty. *) + + val max_interval : t -> interval + (** [max_interval t] returns the largest (in terms of the ordering) interval in [t], or raises [Not_found] if the set is empty. *) val choose : t -> interval @@ -128,10 +136,22 @@ module type INTERVAL_SET = sig val inter : t -> t -> t (** set intersection *) + val subset : t -> t -> bool + (** subsets *) + val find_next_gap : elt -> t -> elt (** [find_next_gap from t] returns the next element that's absent in set [t] and greater than or equal to [from] **) + val elements : t -> interval list + (** [elements t] returns the list of intervals in the set [t]. *) + + val elements_individual : t -> elt list + (** [elements_individual t] returns the list of elements in the set [t]. *) + + val of_list : elt list -> t + (** [of_list li] returns the set of elements in the list [li]. *) + (**/**) val check_invariants : t -> (unit, string) result diff --git a/asllib/types.ml b/asllib/types.ml index b4cfd77fe..d7ca93bf6 100644 --- a/asllib/types.ml +++ b/asllib/types.ml @@ -346,173 +346,126 @@ module Domain = struct let compare _d1 _d2 = assert false - module Iterators = struct + (** The [StaticApprox] module creates constant approximation of integer + constraints as sets of integers. *) + module StaticApprox = struct + (** The two possible types of approximations. *) type approx = Over | Under exception CannotOverApproximate - - let assert_under approx acc = - if approx = Over then raise CannotOverApproximate else acc - - let fold_zs = - let rec aux f z1 z2 acc = - if Z.lt z2 z1 then acc else f z1 acc |> aux f (Z.succ z1) z2 + (** Raised if over approximation is not possible. *) + + (** Util to raise [CannotOverApproximate]. *) + let assert_under approx = + if approx = Over then raise CannotOverApproximate else IntSet.empty + + let make_interval approx z1 z2 = + if Z.leq z1 z2 then IntSet.(add (Interval.make z1 z2) empty) + else assert_under approx + + let intset_map f s = + IntSet.elements_individual s |> List.map f |> IntSet.of_list + + let intset_cross_map f s1 s2 = + let l1 = IntSet.elements_individual s1 + and l2 = IntSet.elements_individual s2 in + list_cross f l1 l2 |> IntSet.of_list + + let literal_to_z = function L_Int z -> z | _ -> assert false + + let apply_unop loc op z = + Operations.unop_values loc Error.Static op (L_Int z) |> literal_to_z + + let apply_binop loc op z1 z2 = + Operations.binop_values loc Error.Static op (L_Int z1) (L_Int z2) + |> literal_to_z + + let iterated op = + let rec pairwise acc = function + | [] -> acc + | [ x ] -> x :: acc + | x :: y :: t -> pairwise (op x y :: acc) t + and iter = function + | [] -> raise (Invalid_argument "iterated") + | [ x ] -> x + | li -> pairwise [] li |> iter in - fun f z1 z2 acc -> - match Z.compare z1 z2 with - | 1 -> acc - | 0 -> f z1 acc - | -1 -> acc |> f z1 |> f z2 |> aux f (Z.succ z1) (Z.pred z2) - | _ -> assert false - - let rec expr_fold : - 'acc. _ -> _ -> (literal -> 'acc -> 'acc) -> _ -> 'acc -> 'acc = - fun approx env f e acc -> - let e = StaticModel.try_normalize env e in + iter + + let rec approx_expr approx env e = match e.desc with - | E_Literal l -> f l acc - | E_Var x -> - if approx = Over then - let t = try SEnv.type_of env x with Not_found -> assert false in - type_fold Over env f t acc - else acc - | E_Unop (op, e) -> - let f' z = Operations.unop_values e Error.Static op z |> f in - expr_fold approx env f' e acc + | E_Literal (L_Int z) -> IntSet.singleton z + | E_Literal _ -> assert_under approx + | E_Var x -> ( + match approx with + | Over -> approx_type Over env (SEnv.type_of env x) + | Under -> IntSet.empty) + | E_Unop (op, e') -> + intset_map (apply_unop e op) (approx_expr approx env e') | E_Binop (op, e1, e2) -> - let f1 z2 z1 = Operations.binop_values e Error.Static op z1 z2 |> f in - let f2 z2 = expr_fold approx env (f1 z2) e1 in - expr_fold approx env f2 e2 acc - | E_Arbitrary t -> type_fold approx env f t acc - | E_Cond (e1, e2, e3) -> - let f' = function - | L_Bool b -> expr_fold approx env f (if b then e2 else e3) - | _ -> - assert false (* Type error - should have been caught earlier. *) - in - expr_fold approx env f' e1 acc - | E_Array _ | E_EnumArray _ | E_GetArray _ | E_GetEnumArray _ - | E_GetField _ | E_GetFields _ | E_GetItem _ | E_Record _ | E_Tuple _ -> - (* Not supported: aggregate types. *) - assert_under approx acc - | E_ATC (_, _) | E_Slice (_, _) | E_Pattern (_, _) | E_Call _ -> - (* Not yet implemented *) - assert_under approx acc - - and type_fold : - 'acc. _ -> _ -> (literal -> 'acc -> 'acc) -> _ -> 'acc -> 'acc = - fun approx env f t acc -> - let t = make_anonymous env t in + intset_cross_map (apply_binop e op) + (approx_expr approx env e1) + (approx_expr approx env e2) + | E_Arbitrary t -> approx_type approx env t + | E_Cond _ -> (* Not yet implemented *) assert_under approx + | _ -> assert_under approx + + and approx_type approx env t = match t.desc with - | T_Real | T_String | T_Int (UnConstrained | Parameterized _) -> - assert_under approx acc (* We can't iterate on all of those. *) + | T_Named _ -> make_anonymous env t |> approx_type approx env + | T_Int (WellConstrained cs) -> approx_constraints approx env cs | T_Int PendingConstrained -> assert false - | T_Int (WellConstrained cs) -> constraints_fold approx env f cs acc - | T_Bool -> acc |> f (L_Bool true) |> f (L_Bool false) - | T_Bits (e_len, _) -> - let f1 length z = L_BitVector (Bitvector.of_z length z) |> f in - let f2 = function - | L_Int z when Z.fits_int z && Z.sign z >= 0 -> - let length = Z.to_int z in - let max = Z.shift_left Z.one length |> Z.pred in - fold_zs (f1 length) Z.zero max - | L_Int _ -> Fun.id (* Those are delayed until runtime. *) - | _ -> assert false (* Type error. *) - in - expr_fold approx env f2 e_len acc - | T_Enum li -> - List.fold_left - (fun acc x -> - expr_fold approx env f (E_Var x |> add_pos_from t) acc) - acc li - | T_Tuple _ | T_Array (_, _) | T_Record _ | T_Exception _ -> - (* Non supported: aggregate types. *) - assert_under approx acc - | T_Named _ -> assert false (* Error in output of [make_anonmymous]. *) - - and constraint_fold : - 'acc. _ -> _ -> (literal -> 'acc -> 'acc) -> _ -> 'acc -> 'acc = - fun approx env f c acc -> - match c with - | Constraint_Exact e -> expr_fold approx env f e acc - | Constraint_Range (e1, e2) -> - let z1, z2 = - match approx with - | Over -> (get_min env e1, get_max env e2) - | Under -> (get_max env e1, get_min env e2) - in - let f z = f (L_Int z) in - fold_zs f z1 z2 acc - - and constraints_fold : - 'acc. _ -> _ -> (literal -> 'acc -> 'acc) -> _ -> 'acc -> 'acc = - fun approx env f li acc -> - List.fold_left (fun acc c -> constraint_fold approx env f c acc) acc li - - and get_min env e = - expr_fold Over env - (function L_Int z1 -> Z.min z1 | _ -> assert false) - e - Z.(shift_left one 30) - - and get_max env e = - expr_fold Over env - (function L_Int z1 -> Z.max z1 | _ -> assert false) - e - Z.(shift_left minus_one 30) - - let constraints_for_all env is f = - let exception FalseFound in - let f' l _acc = f l || raise FalseFound in - try constraints_fold Over env f' is true - with CannotOverApproximate | FalseFound -> false - - let constraints_exists env is f = - let exception TrueFound in - let f' l _acc = f l && raise TrueFound in - try constraints_fold Under env f' is false with - | CannotOverApproximate -> false - | TrueFound -> true + | T_Real | T_String | T_Int (UnConstrained | Parameterized _) -> + assert_under approx (* We can't iterate on those. *) + | T_Bool | T_Bits _ | T_Enum _ -> + (* Not yet implemented *) assert_under approx + | _ -> assert false + + and approx_constraints approx env cs = + let op = + match approx with Under -> IntSet.inter | Over -> IntSet.union + in + List.map (approx_constraint approx env) cs |> iterated op + + and approx_constraint approx env = function + | Constraint_Exact e -> approx_expr approx env e + | Constraint_Range (e1, e2) -> ( + try + let z1, z2 = + match approx with + | Over -> (get_min env e1, get_max env e2) + | Under -> (get_max env e1, get_min env e2) + in + make_interval approx z1 z2 + with Not_found | CannotOverApproximate -> assert_under approx) + + and get_min env e = approx_expr Over env e |> IntSet.min_elt + and get_max env e = approx_expr Over env e |> IntSet.max_elt end - let int_set_for_all = - let interval_iter elt_iter interval = - let x = IntSet.Interval.x interval and y = IntSet.Interval.y interval in - (* We try the extremities first, in case it's linear. *) - elt_iter x; - elt_iter y; - let n = Z.(sub y x |> to_int) in - for i = 0 to n do - Z.of_int i |> Z.add x |> elt_iter - done - in - let exception FalseFound in - fun is f -> - let elt_iter z = if f z then () else raise FalseFound in - try - IntSet.iter (interval_iter elt_iter) is; - true - with FalseFound -> false - (* Begin SymIntSetSubset *) let int_set_is_subset env is1 is2 = + let open StaticApprox in match (is1, is2) with | _, Top -> true |: TypingRule.SymIntSetSubset | Top, _ -> false | Finite ints1, Finite ints2 -> IntSet.(is_empty (diff ints1 ints2)) - | FromSyntax cs1, FromSyntax cs2 -> + | FromSyntax cs1, FromSyntax cs2 -> ( constraints_equal env cs1 cs2 - || Iterators.constraints_for_all env cs1 @@ fun l1 -> - Iterators.constraints_exists env cs2 @@ fun l2 -> literal_equal l1 l2 - | Finite ints1, FromSyntax cs2 -> ( - int_set_for_all ints1 @@ fun z1 -> - Iterators.constraints_exists env cs2 @@ function - | L_Int z2 -> Z.equal z1 z2 - | _ -> false) - | FromSyntax cs1, Finite ints2 -> ( - Iterators.constraints_for_all env cs1 @@ function - | L_Int z1 -> IntSet.mem z1 ints2 - | _ -> false) + || + try + let s1 = approx_constraints Over env cs1 + and s2 = approx_constraints Under env cs2 in + IntSet.subset s1 s2 + with CannotOverApproximate -> false) + | Finite s1, FromSyntax cs2 -> + let s2 = approx_constraints Under env cs2 in + IntSet.subset s1 s2 + | FromSyntax cs1, Finite s2 -> ( + try + let s1 = approx_constraints Over env cs1 in + IntSet.subset s1 s2 + with CannotOverApproximate -> false) (* End *) (* Begin SyDomIsSubset *)