Commit 80620fde authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Check constraints on monomorphic variables at the right place.

parent ce75822e
...@@ -285,12 +285,12 @@ struct ...@@ -285,12 +285,12 @@ struct
times = BoolPair.full; times = BoolPair.full;
xml = BoolPair.full; xml = BoolPair.full;
arrow = BoolPair.full; arrow = BoolPair.full;
record= BoolRec.full; record = BoolRec.full;
ints = BoolIntervals.full; ints = BoolIntervals.full;
atoms = BoolAtoms.full; atoms = BoolAtoms.full;
chars = BoolChars.full; chars = BoolChars.full;
abstract = BoolAbstracts.full; abstract = BoolAbstracts.full;
absent= false; absent = false;
} }
let check a = let check a =
...@@ -398,7 +398,8 @@ type descr = Descr.t ...@@ -398,7 +398,8 @@ type descr = Descr.t
type node = Node.t type node = Node.t
include Descr include Descr
let forward_print = ref (fun _ _ -> assert false) let dummy_print = (fun _ _ -> assert false)
let forward_print = ref dummy_print
let make () = let make () =
incr count; incr count;
...@@ -452,15 +453,6 @@ let char c = { empty with chars = BoolChars.atom (`Atm c) } ...@@ -452,15 +453,6 @@ let char c = { empty with chars = BoolChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) } let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
let abstract a = { empty with abstract = BoolAbstracts.atom (`Atm a) } let abstract a = { empty with abstract = BoolAbstracts.atom (`Atm a) }
module type BVS =
sig
type elem
type t
val get : t -> (elem list* elem list) list
end
let cup x y = let cup x y =
if x == y then x else if x == y then x else
{ {
...@@ -481,7 +473,7 @@ let cap x y = ...@@ -481,7 +473,7 @@ let cap x y =
ints = BoolIntervals.cap x.ints y.ints; ints = BoolIntervals.cap x.ints y.ints;
times = BoolPair.cap x.times y.times; times = BoolPair.cap x.times y.times;
xml = BoolPair.cap x.xml y.xml; xml = BoolPair.cap x.xml y.xml;
record= BoolRec.cap x.record y.record; record = BoolRec.cap x.record y.record;
arrow = BoolPair.cap x.arrow y.arrow; arrow = BoolPair.cap x.arrow y.arrow;
atoms = BoolAtoms.cap x.atoms y.atoms; atoms = BoolAtoms.cap x.atoms y.atoms;
chars = BoolChars.cap x.chars y.chars; chars = BoolChars.cap x.chars y.chars;
...@@ -877,7 +869,8 @@ let rec slot d = ...@@ -877,7 +869,8 @@ let rec slot d =
then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars))) then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars)))
else if not (Abstracts.is_empty (BoolAbstracts.leafconj d.abstract)) else if not (Abstracts.is_empty (BoolAbstracts.leafconj d.abstract))
then slot_nempty (Witness.WAbstract (Abstracts.sample (BoolAbstracts.leafconj d.abstract))) then slot_nempty (Witness.WAbstract (Abstracts.sample (BoolAbstracts.leafconj d.abstract)))
else try DescrHash.find memo d else try
DescrHash.find memo d
with Not_found -> with Not_found ->
let s = { status = Maybe; active = false; notify = Nothing } in let s = { status = Maybe; active = false; notify = Nothing } in
DescrHash.add memo d s; DescrHash.add memo d s;
...@@ -1009,12 +1002,17 @@ let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1) ...@@ -1009,12 +1002,17 @@ let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)
(* functions on variables need the subtyping relation *) (* functions on variables need the subtyping relation *)
let get_variables =
let memo_descr = DescrHash.create 17 in module type BVS =
fun t -> sig
type elem
type t
val get : t -> (elem list* elem list) list
end
let get_variables main_memo temp_memo t =
let get_vars_conj get_atom pos acc l = let get_vars_conj get_atom pos acc l =
List.fold_left (fun acc e -> List.fold_left (fun acc e -> get_atom pos acc e) acc l
get_atom pos acc e) acc l
in in
let get_vars_bdd (type s) (type e) let get_vars_bdd (type s) (type e)
(module BV : BVS with type elem = e and type t = s) (module BV : BVS with type elem = e and type t = s)
...@@ -1048,37 +1046,44 @@ let get_variables = ...@@ -1048,37 +1046,44 @@ let get_variables =
and get_variables pos (tvpos,tvneg,vars) t = and get_variables pos (tvpos,tvneg,vars) t =
let tpos, tneg, tvars = let tpos, tneg, tvars =
try try
let r = DescrHash.find memo_descr t in DescrHash.find main_memo t
r
with with
Not_found -> Not_found -> begin
let acc = Var.Set.(empty,empty,empty) in try DescrHash.find temp_memo t with
DescrHash.add memo_descr t acc; Not_found ->
let acc = get_vars_bdd (module BoolIntervals) let acc = Var.Set.(empty,empty,empty) in
(get_vars_boolvar get_nothing) pos acc t.ints in DescrHash.add temp_memo t acc;
let acc = get_vars_bdd (module BoolChars) let acc = get_vars_bdd (module BoolIntervals)
(get_vars_boolvar get_nothing) pos acc t.chars in (get_vars_boolvar get_nothing) pos acc t.ints in
let acc = get_vars_bdd (module BoolAtoms) let acc = get_vars_bdd (module BoolChars)
(get_vars_boolvar get_nothing) pos acc t.atoms in (get_vars_boolvar get_nothing) pos acc t.chars in
let acc = get_vars_bdd (module BoolAbstracts) let acc = get_vars_bdd (module BoolAtoms)
(get_vars_boolvar get_nothing) pos acc t.abstract in (get_vars_boolvar get_nothing) pos acc t.atoms in
let acc = get_bv_pairs pos acc t.times in let acc = get_vars_bdd (module BoolAbstracts)
let acc = get_bv_pairs pos acc t.xml in (get_vars_boolvar get_nothing) pos acc t.abstract in
let acc = get_bv_pairs pos acc t.arrow in let acc = get_bv_pairs pos acc t.times in
let acc = get_bv_recs pos acc t.record in let acc = get_bv_pairs pos acc t.xml in
DescrHash.replace memo_descr t acc; let acc = get_bv_pairs pos acc t.arrow in
acc let acc = get_bv_recs pos acc t.record in
DescrHash.replace temp_memo t acc;
acc
end
in in
(Var.Set.union tvpos tpos, (Var.Set.union tvpos tpos,
Var.Set.union tvneg tneg, Var.Set.union tvneg tneg,
Var.Set.union tvars vars) Var.Set.union tvars vars)
in in
try get_variables true Var.Set.(empty,empty,empty) t
DescrHash.find memo_descr t
with let get_variables =
Not_found -> let main_memo = DescrHash.create 17 in
let res = get_variables true Var.Set.(empty,empty,empty) t in fun t ->
DescrHash.add memo_descr t res; try DescrHash.find main_memo t
with Not_found ->
let res = get_variables main_memo (DescrHash.create 17) t in
DescrHash.add main_memo t res;
res res
let check_var = let check_var =
...@@ -1810,7 +1815,7 @@ struct ...@@ -1810,7 +1815,7 @@ struct
trivial_pair d.arrow && trivial_rec d.record) trivial_pair d.arrow && trivial_rec d.record)
let worth_complement d = let worth_complement d =
let aux f x y = if f x y = 0 then 1 else 0 in let aux f x y = if f x y = 0 then 1 else 0 in
let n = let n =
aux BoolAtoms.compare d.atoms any.atoms + aux BoolAtoms.compare d.atoms any.atoms +
aux BoolChars.compare d.chars any.chars + aux BoolChars.compare d.chars any.chars +
...@@ -1914,8 +1919,9 @@ struct ...@@ -1914,8 +1919,9 @@ struct
false, res false, res
with Not_found -> true, [ Key.empty , any ] with Not_found -> true, [ Key.empty , any ]
in in
if found_any then (slot.def <- [Neg (alloc [])];slot) if found_any then begin
else (slot.def <- [Neg (alloc [])];slot)
end else
let merge_column_with (v1,t1) l = let merge_column_with (v1,t1) l =
List.fold_left (fun (accv, accl) ((v2,t2) as x) -> List.fold_left (fun (accv, accl) ((v2,t2) as x) ->
if equal t1 t2 then (v2::accv, accl) else (accv,x::accl)) if equal t1 t2 then (v2::accv, accl) else (accv,x::accl))
...@@ -2003,7 +2009,7 @@ struct ...@@ -2003,7 +2009,7 @@ struct
| l, [] -> [ inter_nd l ] | l, [] -> [ inter_nd l ]
| l1, l2 -> [ Diff (alloc [inter_nd l1], alloc l2) ] | l1, l2 -> [ Diff (alloc [inter_nd l1], alloc l2) ]
in in
if subtype any tt then print_topvars true [] else (*if subtype any tt then print_topvars true [] else*)
let tt, positive = let tt, positive =
if worth_complement tt then if worth_complement tt then
diff any tt, false diff any tt, false
...@@ -2776,8 +2782,8 @@ module Positive = struct ...@@ -2776,8 +2782,8 @@ module Positive = struct
with with
Not_found -> Not_found ->
let node_t = forward () in let node_t = forward () in
(*if no_var t then ty t if no_var t then ty t
else *) else
let () = DescrHash.add memo t node_t in let () = DescrHash.add memo t node_t in
let descr_t = let descr_t =
decompose_kind Atom.any atom (BoolAtoms.get t.atoms) decompose_kind Atom.any atom (BoolAtoms.get t.atoms)
...@@ -3050,7 +3056,7 @@ module Tallying = struct ...@@ -3050,7 +3056,7 @@ module Tallying = struct
let inter delta map1 map2 = VarMap.fold (add delta) map1 map2 let inter delta map1 map2 = VarMap.fold (add delta) map1 map2
let fold = VarMap.fold let fold = VarMap.fold
let empty = VarMap.empty let empty = VarMap.empty
let for_all = VarMap.for_all
end end
(* equation set : (s < alpha < t) stored as (* equation set : (s < alpha < t) stored as
...@@ -3171,7 +3177,7 @@ module Tallying = struct ...@@ -3171,7 +3177,7 @@ module Tallying = struct
add merged acc2 add merged acc2
) )
s2 acc1) s1 [] s2 acc1) s1 []
let filter = List.filter
end end
type s = S.t type s = S.t
...@@ -3189,27 +3195,13 @@ module Tallying = struct ...@@ -3189,27 +3195,13 @@ module Tallying = struct
type sl = sigma list type sl = sigma list
let singleton delta c = let singleton _delta c =
let constr, do_check, t1, t2 = let constr =
match c with match c with
|Pos (v,s) -> |Pos (v,s) -> M.singleton v (empty,s)
if Var.Set.mem v delta then M.empty, true, (var v), s |Neg (s,v) -> M.singleton v (s,any)
else M.singleton v (empty,s), false, empty, empty
|Neg (s,v) ->
if Var.Set.mem v delta then M.empty, true, s, (var v)
else M.singleton v (s,any), false, empty, empty
in in
let res = S.singleton constr in S.singleton constr
if do_check then
if subtype t1 t2 then res
else
raise (UnSatConstr
(Format.sprintf
"Constraint (%s) <= (%s) on monomorphic variable failed"
(Utils.string_of_formatter Print.pp_type t1)
(Utils.string_of_formatter Print.pp_type t2)
))
else res
let pp_s = S.pp let pp_s = S.pp
let pp_m = M.pp let pp_m = M.pp
...@@ -3260,7 +3252,8 @@ module Tallying = struct ...@@ -3260,7 +3252,8 @@ module Tallying = struct
let single_arrow = single_aux (fun p -> { empty with arrow = BoolPair.atom (`Atm p) }) let single_arrow = single_aux (fun p -> { empty with arrow = BoolPair.atom (`Atm p) })
(* check if there exists a toplevel varaible : fun (pos,neg) *) (* check if there exists a toplevel varaible : fun (pos,neg) *)
let toplevel delta single norm_rec mem p n = match (p,n) with let toplevel delta single norm_rec mem p n =
match (p,n) with
|([],(`Var x)::neg) -> |([],(`Var x)::neg) ->
let t = single (false,x,[],neg) in let t = single (false,x,[],neg) in
CS.singleton delta (Neg (t,`Var x)) CS.singleton delta (Neg (t,`Var x))
...@@ -3299,7 +3292,7 @@ module Tallying = struct ...@@ -3299,7 +3292,7 @@ module Tallying = struct
let rec norm (t,delta,mem) = let rec norm (t,delta,mem) =
debug_norm "Calling norm on input type %a : " Print.pp_type t; debug_norm "Calling norm on input type %a : " Print.pp_type t;
(* if we already evaluated it, it is sat *) (* if we already evaluated it, it is sat *)
if DescrSet.mem t mem || is_empty t then begin if DescrSet.mem t mem || is_empty t then begin
debug_norm "It's Empty or found in memo, SAT@\n%!" ; debug_norm "It's Empty or found in memo, SAT@\n%!" ;
(*Format.printf "Sat for type %a\n%!" Print.print t; *) (*Format.printf "Sat for type %a\n%!" Print.print t; *)
CS.sat CS.sat
...@@ -3307,7 +3300,7 @@ module Tallying = struct ...@@ -3307,7 +3300,7 @@ module Tallying = struct
(* if there is only one variable then is it A <= 0 or 1 <= A *) (* if there is only one variable then is it A <= 0 or 1 <= A *)
if is_var t then begin if is_var t then begin
debug_norm "It's a variable " ; debug_norm "It's a variable " ;
let (v,p) = TLV.max t.toplvars in let (v,p) = extract_variable t in
if Var.Set.mem v delta then begin if Var.Set.mem v delta then begin
debug_norm "which is in delta, UNSAT@\n%!" ; debug_norm "which is in delta, UNSAT@\n%!" ;
CS.unsat CS.unsat
...@@ -3325,8 +3318,7 @@ module Tallying = struct ...@@ -3325,8 +3318,7 @@ module Tallying = struct
debug_norm "It is a complex type, adding to memo and recursing @\n%!"; debug_norm "It is a complex type, adding to memo and recursing @\n%!";
let mem = DescrSet.add t mem in let mem = DescrSet.add t mem in
let aux single norm_aux acc l = let aux single norm_aux acc l =
let res = big_prod delta (toplevel delta single norm_aux mem) acc l let res = big_prod delta (toplevel delta single norm_aux mem) acc l in
in
debug_norm " For type (%a) constraints where %a, are now %a@\n%!" Print.pp_type t CS.pp_s acc CS.pp_s res; res debug_norm " For type (%a) constraints where %a, are now %a@\n%!" Print.pp_type t CS.pp_s acc CS.pp_s res; res
in in
let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
...@@ -3338,8 +3330,16 @@ module Tallying = struct ...@@ -3338,8 +3330,16 @@ module Tallying = struct
let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
(* XXX normrec is not tested at all !!! *) (* XXX normrec is not tested at all !!! *)
let res = aux single_record normrec acc (BoolRec.get t.record) in let res = aux single_record normrec acc (BoolRec.get t.record) in
let res =
CS.S.filter
(fun m -> CS.M.for_all (fun v (s, t) -> not (Var.Set.mem v delta) ||
let x = var v in subtype s x && subtype x t
) m)
res
in
debug_norm "Type (%a) yielded constraints: %a@\n%!" debug_norm "Type (%a) yielded constraints: %a@\n%!"
Print.pp_type t CS.pp_s res; res Print.pp_type t CS.pp_s res; res
end end
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P (* (t1,t2) = intersection of all (fst pos,snd pos) \in P
...@@ -3435,14 +3435,11 @@ module Tallying = struct ...@@ -3435,14 +3435,11 @@ module Tallying = struct
in in
big_prod delta norm_arrow CS.sat (Pair.get t) big_prod delta norm_arrow CS.sat (Pair.get t)
module NormMemoHash = Hashtbl.Make(
struct
type t = (Descr.t * Var.Set.t)
let hash (v,d) = Descr.hash v + Var.Set.hash d
let equal (v1,d1) (v2,d2) = Descr.equal v1 v2 && Var.Set.equal d1 d2
end )
module NormMemoHash = Hashtbl.Make(Custom.Pair(Descr)(Var.Set))
let memo_norm = NormMemoHash.create 17 let memo_norm = NormMemoHash.create 17
let norm delta t = let norm delta t =
try NormMemoHash.find memo_norm (t,delta) try NormMemoHash.find memo_norm (t,delta)
with Not_found -> begin with Not_found -> begin
...@@ -3455,7 +3452,7 @@ module Tallying = struct ...@@ -3455,7 +3452,7 @@ module Tallying = struct
let res = let res =
CS.M.fold (fun v (inf, sup) acc -> CS.M.fold (fun v (inf, sup) acc ->
(* no need to add new constraints *) (* no need to add new constraints *)
if subtype inf sup then acc if subtype inf sup then acc
else else
let x = diff inf sup in let x = diff inf sup in
if DescrHash.mem mem x then acc if DescrHash.mem mem x then acc
...@@ -3474,13 +3471,15 @@ module Tallying = struct ...@@ -3474,13 +3471,15 @@ module Tallying = struct
let merge delta m = merge (m,delta,DescrHash.create 17) let merge delta m = merge (m,delta,DescrHash.create 17)
(* Add constraints of the form { alpha = ( s v fresh ) ^ t } *) (* Add constraints of the form { alpha = ( s v fresh ) ^ t } *)
let solve s = let solve s =
let aux ((`Var v) as alpha) (s,t) acc = let aux ((`Var v) as alpha) (s,t) acc =
(* we cannot solve twice the same variable *) (* we cannot solve twice the same variable *)
assert(not(CS.E.mem alpha acc)); assert(not(CS.E.mem alpha acc));
let pre = Printf.sprintf "#fr_%s_" (Var.id alpha) in let pre = Printf.sprintf "#fr_%s_" (Var.id alpha) in
let b = var (Var.fresh ~pre ()) in let b = var (Var.fresh ~pre ()) in
(* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *) (* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *)
CS.E.add alpha (cap (cup s b) t) acc CS.E.add alpha (cap (cup s b) t) acc
in in
let aux1 m = let aux1 m =
...@@ -3543,6 +3542,7 @@ module Tallying = struct ...@@ -3543,6 +3542,7 @@ module Tallying = struct
else CS.prod delta acc (norm delta d) else CS.prod delta acc (norm delta d)
) CS.sat l ) CS.sat l
in in
debug_norm "First step gave constraints: %a@\n%!" CS.pp_s n;
if Pervasives.(n = CS.unsat) then raise Step1Fail else if Pervasives.(n = CS.unsat) then raise Step1Fail else
let m = let m =
CS.S.fold (fun c acc -> CS.S.fold (fun c acc ->
...@@ -3658,6 +3658,7 @@ let squaresubtype delta s t = ...@@ -3658,6 +3658,7 @@ let squaresubtype delta s t =
in in
set ai i ss; set ai i ss;
tallying i; tallying i;
if i == 2 then raise (Tallying.UnSatConstr "Gave up");
loop (i+1) loop (i+1)
with FoundSquareSub sl -> sl with FoundSquareSub sl -> sl
in in
...@@ -3709,6 +3710,7 @@ let apply_raw delta s t = ...@@ -3709,6 +3710,7 @@ let apply_raw delta s t =
tallying i j; tallying i j;
done; done;
tallying i i; tallying i i;
if i == 2 then raise (Tallying.UnSatConstr "Gave up");
loop (i+1) loop (i+1)
with FoundApply (res, i, j, sl) -> sl, get ai i, get aj j, res with FoundApply (res, i, j, sl) -> sl, get ai i, get aj j, res
in in
......
...@@ -86,13 +86,13 @@ include Custom.T ...@@ -86,13 +86,13 @@ include Custom.T
module Node : Custom.T module Node : Custom.T
module Pair : Bool.S with type elem = (Node.t * Node.t) module Pair : Bool.S with type elem = (Node.t * Node.t)
module BoolPair : BoolVar.S with module BoolPair : BoolVar.S with
type s = Pair.t and type s = Pair.t and
type elem = Pair.t Var.pairvar type elem = Pair.t Var.pairvar
module Rec : Bool.S with type elem = bool * Node.t Ident.label_map module Rec : Bool.S with type elem = bool * Node.t Ident.label_map
module BoolRec : BoolVar.S with module BoolRec : BoolVar.S with
type s = Rec.t and type s = Rec.t and
type elem = Rec.t Var.pairvar type elem = Rec.t Var.pairvar
type descr = t type descr = t
...@@ -442,7 +442,7 @@ module Tallying : sig ...@@ -442,7 +442,7 @@ module Tallying : sig
|S of CS.sigma (** Substitution *) |S of CS.sigma (** Substitution *)
|A of (symsubst * symsubst) (** Composition si (sj t) *) |A of (symsubst * symsubst) (** Composition si (sj t) *)
(** Cartesian Product of two symbolic substitution sets *) (** Cartesian Product of two symbolic substitution sets *)
val ( ++ ) : symsubst list -> symsubst list -> symsubst list val ( ++ ) : symsubst list -> symsubst list -> symsubst list
(** Evaluation of a substitution *) (** Evaluation of a substitution *)
...@@ -454,8 +454,8 @@ module Tallying : sig ...@@ -454,8 +454,8 @@ module Tallying : sig
end end
(** Square Subtype relation. [squaresubtype delta s t] . (** Square Subtype relation. [squaresubtype delta s t] .
True if there exists a substitution such that s < t only True if there exists a substitution such that s < t only
considering variables that are not in delta *) considering variables that are not in delta *)
val squaresubtype : Var.Set.t -> t -> t -> Tallying.CS.sl val squaresubtype : Var.Set.t -> t -> t -> Tallying.CS.sl
val is_squaresubtype : Var.Set.t -> t -> t -> bool val is_squaresubtype : Var.Set.t -> t -> t -> bool
...@@ -469,4 +469,3 @@ val apply_full : Var.Set.t -> t -> t -> t ...@@ -469,4 +469,3 @@ val apply_full : Var.Set.t -> t -> t -> t
val apply_raw : Var.Set.t -> t -> t -> Tallying.CS.sl * t * t * t val apply_raw : Var.Set.t -> t -> t -> Tallying.CS.sl * t * t * t
val squareapply : Var.Set.t -> t -> t -> (Tallying.CS.sl * t) val squareapply : Var.Set.t -> t -> t -> (Tallying.CS.sl * t)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment