Skip to content

GitLab

Commit ec80900d authored by Pietro Abate's avatar Pietro Abate
Browse files

Convert Descr.Abstrat to a BooVar Bdd 

Tallying and printing still broken.
parent 4696df52
Hide whitespace changes
Inline Side-by-side
Showing with 97 additions and 81 deletions
ocamliface/mlstub.ml
View file @ ec80900d
......@@ -75,7 +75,7 @@ and typ_descr = function
| Abstract "int" -> Builtin_defs.caml_int
| Abstract "char" -> Builtin_defs.char_latin1
| Abstract "string" -> Builtin_defs.string_latin1
| Abstract s -> Types.abstract (Types.Abstract.atom s)
| Abstract s -> Types.abstract (Types.Abstracts.atom s)
| Builtin ("list", [t])
| Builtin ("array", [t]) -> Types.descr (Sequence.star_node (typ t))
| Builtin ("Pervasives.ref", [t]) -> Builtin_defs.ref_type (typ t)
......
parser/parser.ml
View file @ ec80900d
......@@ -614,7 +614,7 @@ EXTEND Gram
| "("; a = IDENT; ":="; c = expr; ")" ->
mk _loc (Constant (ident a,c))
| "!"; a = IDENT ->
mk _loc (Internal (Types.abstract (Types.Abstract.atom a)))
mk _loc (Internal (Types.abstract (Types.Abstracts.atom a)))
| ids = LIST1 ident_or_keyword SEP "." ->
let ids = List.map (fun x -> ident x) ids in
mk _loc (PatVar ids)
......
runtime/run_dispatch.ml
View file @ ec80900d
......@@ -250,7 +250,7 @@ and run_disp_kind env actions v =
| Abstraction (Some iface,_,sigma) ->
run_disp_basic v (fun t -> inzero env v t) actions.basic
| Abstract (abs,_) ->
run_disp_basic v (fun t -> Types.Abstract.contains abs (Types.get_abstract t))
run_disp_basic v (fun t -> Types.Abstract.has_abstract t abs (* Types.Abstracts.contains abs (Types.Abstract.get t) *))
actions.basic
| Absent ->
run_disp_basic v (fun t -> Types.Record.has_absent t) actions.basic
......
runtime/value.ml
View file @ ec80900d
......@@ -18,7 +18,7 @@ and t =
| Integer of Intervals.V.t
| Char of Chars.V.t
| Abstraction of (Types.descr * Types.descr) list option * (t -> t) * sigma
| Abstract of Types.Abstract.V.t
| Abstract of Types.Abstracts.V.t
| String_latin1 of int * int * string * t
| String_utf8 of Utf8.uindex * Utf8.uindex * Utf8.t * t
| Concat of t * t
......@@ -531,7 +531,7 @@ let rec compare x y =
| _, Abstraction (_,_,_) ->
raise (CDuceExn (string_latin1 "comparing functional values"))
| Abstract (s1,v1), Abstract (s2,v2) ->
let c = Types.Abstract.T.compare s1 s2 in if c <> 0 then c
let c = Types.Abstracts.T.compare s1 s2 in if c <> 0 then c
else begin
match s1 with
|"float" -> Pervasives.compare (Obj.magic v1 : float) (Obj.magic v2 : float)
......
runtime/value.mli
View file @ ec80900d
......@@ -19,7 +19,7 @@ and t =
| Integer of Intervals.V.t
| Char of Chars.V.t
| Abstraction of (Types.descr * Types.descr) list option * (t -> t) * sigma
| Abstract of Types.Abstract.V.t
| Abstract of Types.Abstracts.V.t
| String_latin1 of int * int * string * t
| String_utf8 of Utf8.uindex * Utf8.uindex * Utf8.t * t
| Concat of t * t
......@@ -73,7 +73,7 @@ val get_field_ascii : t -> string -> t
val get_variant : t -> string * t option
val abstract : Types.Abstract.abs -> 'a -> t
val abstract : Types.Abstracts.abs -> 'a -> t
val get_abstract : t -> 'a
val mk_ref : Types.t -> t -> t
......
tests/libtest/tallyingTest.ml
View file @ ec80900d
......@@ -12,10 +12,9 @@ let parse_typ s =
module ESet = OUnitDiff.SetMake (struct
type t = (Var.var * Types.t)
let compare (v1,t1) (v2,t2) =
let a = Types.abstract Abstract.any in
if (v1,t1) == (v2,t2) then 0
else let c = Var.compare v1 v2 in if c <> 0 then c
else Types.compare (diff t1 a) (diff t2 a)
else Types.compare t1 t2
let pp_printer ppf (v,t) = Format.fprintf ppf "(%a = %a)" Var.pp v Types.Print.pp_type t
let pp_print_sep = OUnitDiff.pp_comma_separator
end)
......
types/builtin_defs.ml
View file @ ec80900d
......@@ -156,7 +156,7 @@ let float_abs =
"float"
let float =
Types.abstract (Types.Abstract.atom float_abs)
Types.abstract (Types.Abstracts.atom float_abs)
let any_attr_node = Types.cons (Types.record_fields (true,LabelMap.empty))
let any_xml,any_xml_seq,any_xml_content =
......
types/builtin_defs.mli
View file @ ec80900d
......@@ -40,7 +40,7 @@ val mk_ref: get:'a -> set:'a -> 'a Ident.label_map
val ref_type: Types.Node.t -> Types.t
val float: Types.t
val float_abs: Types.Abstract.abs
val float_abs: Types.Abstracts.abs
val any_xml : Types.t
......
types/types.ml
View file @ ec80900d
......@@ -102,17 +102,14 @@ module Const = struct
let equal c1 c2 = compare c1 c2 = 0
end
module Abstract =
struct
module Abstracts = struct
module T = Custom.String
type abs = T.t
module V =
struct
type t = abs * Obj.t
end
module V = struct type t = abs * Obj.t end
include SortedList.FiniteCofinite(T)
let full = any
let print = function
| Finite l -> List.map (fun x ppf -> Format.fprintf ppf "!%s" x) l
......@@ -137,6 +134,8 @@ module BoolIntervals : BoolVar.S with
type s = Intervals.t = BoolVar.Make(Intervals)
module BoolChars : BoolVar.S with
type s = Chars.t = BoolVar.Make(Chars)
module BoolAbstracts : BoolVar.S with
type s = Abstracts.t = BoolVar.Make(Abstracts)
module TLV = struct
......@@ -229,7 +228,7 @@ sig
xml : BoolPair.t;
arrow : BoolPair.t;
record: BoolRec.t;
abstract: Abstract.t;
abstract: BoolAbstracts.t;
(* this is used in record to flag the fact that the type of a label is
* absent . It is used for optional arguments in functions as ?Int
* is the union of Int ^ undef where undef is a type with absent : true *)
......@@ -252,7 +251,7 @@ struct
xml : BoolPair.t;
arrow : BoolPair.t;
record: BoolRec.t;
abstract: Abstract.t;
abstract: BoolAbstracts.t;
absent: bool;
toplvars : TLV.t
}
......@@ -267,7 +266,7 @@ struct
BoolPair.dump d.arrow
BoolRec.dump d.record
BoolPair.dump d.xml
Abstract.dump d.abstract
BoolAbstracts.dump d.abstract
d.absent
TLV.dump d.toplvars
......@@ -279,7 +278,7 @@ struct
ints = BoolIntervals.empty;
atoms = BoolAtoms.empty;
chars = BoolChars.empty;
abstract = Abstract.empty;
abstract = BoolAbstracts.empty;
absent= false;
toplvars = TLV.empty
}
......@@ -296,7 +295,7 @@ struct
ints = BoolIntervals.full;
atoms = BoolAtoms.full;
chars = BoolChars.full;
abstract = Abstract.any;
abstract = BoolAbstracts.any;
absent= false;
toplvars = TLV.any
}
......@@ -309,7 +308,7 @@ struct
BoolPair.check a.xml;
BoolPair.check a.arrow;
BoolRec.check a.record;
Abstract.check a.abstract;
BoolAbstracts.check a.abstract;
()
let equal a b =
......@@ -321,7 +320,7 @@ struct
(BoolPair.equal a.xml b.xml) &&
(BoolPair.equal a.arrow b.arrow) &&
(BoolRec.equal a.record b.record) &&
(Abstract.equal a.abstract b.abstract) &&
(BoolAbstracts.equal a.abstract b.abstract) &&
(a.absent == b.absent)
)
......@@ -333,7 +332,7 @@ struct
(BoolPair.is_empty a.xml) &&
(BoolPair.is_empty a.arrow) &&
(BoolRec.is_empty a.record) &&
(Abstract.is_empty a.abstract)
(BoolAbstracts.is_empty a.abstract)
let compare a b =
if a == b then 0
......@@ -344,7 +343,7 @@ struct
else let c = BoolPair.compare a.xml b.xml in if c <> 0 then c
else let c = BoolPair.compare a.arrow b.arrow in if c <> 0 then c
else let c = BoolRec.compare a.record b.record in if c <> 0 then c
else let c = Abstract.compare a.abstract b.abstract in if c <> 0 then c
else let c = BoolAbstracts.compare a.abstract b.abstract in if c <> 0 then c
else if a.absent && not b.absent then -1
else if b.absent && not a.absent then 1
else 0
......@@ -357,7 +356,7 @@ struct
let accu = 17 * accu + BoolPair.hash a.xml in
let accu = 17 * accu + BoolPair.hash a.arrow in
let accu = 17 * accu + BoolRec.hash a.record in
let accu = 17 * accu + Abstract.hash a.abstract in
let accu = 17 * accu + BoolAbstracts.hash a.abstract in
let accu = if a.absent then accu+5 else accu in
accu
......@@ -386,8 +385,8 @@ end
and Pair : Bool.S with type elem = (Node.t * Node.t) =
Bool.Make(Custom.Pair(Node)(Node))
and BoolPair : BoolVar.S with
type s = Pair.t = BoolVar.Make(Pair)
and BoolPair : BoolVar.S with type s = Pair.t =
BoolVar.Make(Pair)
(* bool = true means that the record is open that is, that
* the labels that are not in the domain of the map are
......@@ -467,7 +466,7 @@ let var a = {
ints = BoolIntervals.vars a;
atoms = BoolAtoms.vars a;
chars = BoolChars.vars a;
abstract = Abstract.empty;
abstract = BoolAbstracts.empty;
absent= false;
toplvars = TLV.singleton (a,true)
}
......@@ -519,9 +518,7 @@ let update_tlv x y t =
let char c = { empty with chars = BoolChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
let abstract a = { empty with abstract = a }
let get_abstract t = t.abstract
let abstract a = { empty with abstract = BoolAbstracts.atom (`Atm a) }
let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
......@@ -542,7 +539,7 @@ let cup x y =
ints = BoolIntervals.cup x.ints y.ints;
atoms = BoolAtoms.cup x.atoms y.atoms;
chars = BoolChars.cup x.chars y.chars;
abstract = Abstract.cup x.abstract y.abstract;
abstract = BoolAbstracts.cup x.abstract y.abstract;
absent= x.absent || y.absent;
toplvars = TLV.empty
} in
......@@ -559,7 +556,7 @@ let cap x y =
arrow = BoolPair.cap x.arrow y.arrow;
atoms = BoolAtoms.cap x.atoms y.atoms;
chars = BoolChars.cap x.chars y.chars;
abstract = Abstract.cap x.abstract y.abstract;
abstract = BoolAbstracts.cap x.abstract y.abstract;
absent= x.absent && y.absent;
toplvars = TLV.empty
} in
......@@ -576,7 +573,7 @@ let diff x y =
ints = BoolIntervals.diff x.ints y.ints;
atoms = BoolAtoms.diff x.atoms y.atoms;
chars = BoolChars.diff x.chars y.chars;
abstract = Abstract.diff x.abstract y.abstract;
abstract = BoolAbstracts.diff x.abstract y.abstract;
absent= x.absent && not y.absent;
toplvars = TLV.empty
} in
......@@ -592,7 +589,7 @@ let trivially_disjoint a b =
(BoolPair.trivially_disjoint a.xml b.xml) &&
(BoolPair.trivially_disjoint a.arrow b.arrow) &&
(BoolRec.trivially_disjoint a.record b.record) &&
(Abstract.disjoint a.abstract b.abstract) &&
(BoolAbstracts.trivially_disjoint a.abstract b.abstract) &&
(not (a.absent && b.absent))
let rec constant = function
......@@ -689,7 +686,7 @@ module Witness = struct
| WAtom of Atoms.sample
| WChar of Chars.V.t
| WAbsent
| WAbstract of Abstract.elem option
| WAbstract of Abstracts.elem option
| WPair of witness * witness * witness_slot
| WXml of witness * witness * witness_slot
......@@ -713,7 +710,7 @@ module Witness = struct
| WAtom (Some (_,Some t)) -> 4 + 17 * Ns.Label.hash t
| WAbsent -> 5
| WAbstract None -> 6
| WAbstract (Some t) -> 7 + 17 * Abstract.T.hash t
| WAbstract (Some t) -> 7 + 17 * Abstracts.T.hash t
| WPair (_,_,s)
| WXml (_,_,s)
| WRecord (_,_,s)
......@@ -744,7 +741,7 @@ module Witness = struct
Ns.Label.equal t1 t2
| WAbsent, WAbsent -> true
| WAbstract None, WAbstract None -> false
| WAbstract (Some t1), WAbstract (Some t2) -> Abstract.T.equal t1 t2
| WAbstract (Some t1), WAbstract (Some t2) -> Abstracts.T.equal t1 t2
| _ -> w1 == w2
let equal w1 w2 = match w1,w2 with
......@@ -895,7 +892,7 @@ module Witness = struct
with Exit -> false))
(BoolRec.leafconj t.record)
| WAbsent -> t.absent
| WAbstract a -> Abstract.contains_sample a t.abstract
| WAbstract a -> Abstracts.contains_sample a (BoolAbstracts.leafconj t.abstract)
end
type slot = { mutable status : status;
......@@ -947,6 +944,7 @@ let complex = ref 0
let rec slot d =
incr complex;
Stats.Counter.incr count_subtype;
(* XXX here I call leafconj a zilliontime. REWRITE !!! *)
if d.absent then slot_nempty Witness.WAbsent
else if not (Intervals.is_empty (BoolIntervals.leafconj d.ints))
then slot_nempty (Witness.WInt (Intervals.sample (BoolIntervals.leafconj d.ints)))
......@@ -954,8 +952,8 @@ let rec slot d =
then slot_nempty (Witness.WAtom (Atoms.sample (BoolAtoms.leafconj d.atoms)))
else if not (Chars.is_empty (BoolChars.leafconj d.chars))
then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars)))
else if not (Abstract.is_empty d.abstract)
then slot_nempty (Witness.WAbstract (Abstract.sample d.abstract))
else if not (Abstracts.is_empty (BoolAbstracts.leafconj d.abstract))
then slot_nempty (Witness.WAbstract (Abstracts.sample (BoolAbstracts.leafconj d.abstract)))
else try DescrHash.find memo d
with Not_found ->
let s = { status = Maybe; active = false; notify = Nothing } in
......@@ -1615,7 +1613,7 @@ module Int = struct
let has_int d i = Intervals.contains i (BoolIntervals.leafconj d.ints)
let get d = d.ints
let any = { empty with ints = any.ints }
let any = { empty with ints = BoolIntervals.full }
(* let any = { empty with ints = BoolIntervals.full } *)
end
module Atom = struct
......@@ -1632,6 +1630,12 @@ module Char = struct
let any = { empty with chars = any.chars }
end
module Abstract = struct
let has_abstract d a = Abstracts.contains a (BoolAbstracts.leafconj d.abstract)
let get d = d.abstract
let any = { empty with abstract = any.abstract }
end
module Print =
struct
let rec pp_const ppf = function
......@@ -1764,7 +1768,7 @@ struct
aux BoolPair.compare d.xml any.xml +
aux BoolPair.compare d.arrow any.arrow +
aux BoolRec.compare d.record any.record +
aux Abstract.compare d.abstract any.abstract
aux BoolAbstracts.compare d.abstract any.abstract
in
n >= 5
......@@ -1915,7 +1919,7 @@ struct
(Record (r,some,none))
) (Record.get { empty with record = BoolRec.atom (`Atm x) })) not_seq.toplvars not_seq.record;
List.iter (fun x -> add (Atomic x)) (Abstract.print not_seq.abstract);
List.iter (fun x -> add (Atomic x)) (BoolAbstracts.print not_seq.abstract);
if not_seq.absent then add (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT"));
slot.def <- List.rev slot.def;
......@@ -2390,8 +2394,7 @@ let cond_partition univ qs =
in
List.fold_left add [ univ ] qs
module Positive =
struct
module Positive = struct
module T = struct
type t = descr
let any = any
......@@ -2402,6 +2405,7 @@ struct
let diff = diff
let arrow = arrow
let times = times
let abstract = abstract
let cons = cons
end
......@@ -2458,10 +2462,10 @@ struct
let interval i = ty (interval i)
let char c = ty (char c)
let atom a = ty (atom a)
let abstract a = ty (abstract a)
let record b vlst = cons (`Record (b, vlst))
let define v1 v2 = def v1 (`Cup [v2])
let decompose t =
let memo = DescrHash.create 17 in
let decompose_conj f_atom sign ilist acc =
......@@ -2478,10 +2482,9 @@ struct
| [v] -> v::acc
| l -> (cap l) :: acc) acc dnf
in
let or_var f e =
match e with
(`Var _) as v -> var v
| `Atm a -> f a
let or_var f = function
|(`Var _) as v -> var v
|`Atm a -> f a
in
let decompose_kind any make dnf acc =
decompose_dnf (ty any) (or_var make) dnf acc
......@@ -2518,7 +2521,8 @@ struct
@@ decompose_bdd Product.any times (BoolPair.get t.times)
@@ decompose_bdd Product.any_xml xml (BoolPair.get t.xml)
@@ decompose_bdd Arrow.any arrow (BoolPair.get t.arrow)
@@ decompose_rec Record.any record (BoolRec.get t.record) []
@@ decompose_rec Record.any record (BoolRec.get t.record)
@@ decompose_kind Abstract.any abstract (BoolAbstracts.get t.abstract) []
in
node_t.def <- (cup descr_t).def; node_t
in
......@@ -2554,7 +2558,6 @@ struct
|`Record (b, flst) ->
`Record (b, List.map (fun (b,l,v) -> (b,l,aux v subst)) flst)
|`Neg v -> `Neg (aux v subst)
in
node_v.def <- new_v;
node_v
......@@ -2927,8 +2930,8 @@ module Tallying = struct
type sl = sigma list
let singleton = function
|Pos (v,s) -> S.singleton (M.singleton v (empty,s))
|Neg (s,v) -> S.singleton (M.singleton v (s,any))
|Pos (v,s) -> S.singleton (M.singleton v (empty,s))
|Neg (s,v) -> S.singleton (M.singleton v (s,any))
let pp_s = S.pp
let pp_m = M.pp
......@@ -2947,6 +2950,7 @@ module Tallying = struct
let normatoms (t,_,_) = if Atoms.is_empty t then CS.sat else CS.unsat
let normchars (t,_,_) = if Chars.is_empty t then CS.sat else CS.unsat
let normints (t,_,_) = if Intervals.is_empty t then CS.sat else CS.unsat
let normabstract (t,_,_) = if Abstracts.is_empty t then CS.sat else CS.unsat
let single_aux constr (b,v,p,n) =
let aux f constr l =
......@@ -2958,14 +2962,14 @@ module Tallying = struct
in
let id = (fun x -> x) in
let t = cap (aux id constr p) (aux neg constr n) in
(* XXX the abstract field could be messed up ... maybe *)
if b then (* t = bigdisj ... alpha \in P --> alpha <= neg t *)
{ (neg t) with abstract = Abstract.empty }
else (* t = bigdisj ... alpha \in N --> t <= alpha *)
{ t with abstract = Abstract.empty }
(* t = bigdisj ... alpha \in P --> alpha <= neg t *)
(* t = bigdisj ... alpha \in N --> t <= alpha *)
if b then (neg t) else t
let single_atoms = single_aux atom
let single_abstract = single_aux abstract
let single_chars = single_aux char
let single_ints = single_aux interval
......@@ -3034,6 +3038,7 @@ module Tallying = struct
let acc = aux single_times normpair acc (BoolPair.get t.times) in
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
(* XXX normrec is not tested at all !!! *)
aux single_record normrec acc (BoolRec.get t.record)
......@@ -3386,10 +3391,15 @@ let apply_raw delta s t =
try
let s = get ai i in
let t = arrow (cons (get aj j)) cgamma in
(* Format.printf "Tallying s=%a < t=%a\n" Print.pp_type s Print.pp_type t; *)
let sl = Tallying.tallying ~delta [ (s,t) ] in
let new_res =
Positive.clean_type delta (
List.fold_left (fun tacc si ->
(*
let a = (Tallying.(gamma $$ si)) in
let b = Positive.clean_type delta a in
Format.printf "dirty %a \n clean %a\n" Print.pp_type a Print.pp_type b; *)
cap tacc (Tallying.(gamma $$ si))
) any sl
)
......@@ -3405,7 +3415,7 @@ let apply_raw delta s t =
let (ss,tt) =
if i = 0 then (s,t) else
((cap (Positive.substitutefree delta s) (get ai (i-1))),
(cap (Positive.substitutefree delta t) (get aj (i-1))))
(cap (Positive.substitutefree delta t) (get aj (i-1))))
in
set ai i ss;
set aj i tt;
......
types/types.mli
View file @ ec80900d
open Ident
module BoolAtoms : BoolVar.S with
type s = Atoms.t and
type elem = Atoms.t Var.pairvar
module BoolIntervals : BoolVar.S with
type s = Intervals.t and
type elem = Intervals.t Var.pairvar
module BoolChars : BoolVar.S with
type s = Chars.t and
type elem = Chars.t Var.pairvar
type const =
| Integer of Intervals.V.t
| Atom of Atoms.V.t
......@@ -64,7 +54,7 @@ module CompUnit : sig
end
*)
module Abstract : sig
module Abstracts : sig
module T : Custom.T with type t = string
type abs = T.t
type t
......@@ -72,15 +62,26 @@ module Abstract : sig
val atom: abs -> t
val compare: t -> t -> int
module V : sig
type t = abs * Obj.t
end
module V : sig type t = abs * Obj.t end
val contains: abs -> t -> bool
end
(** Algebra **)
module BoolAtoms : BoolVar.S with
type s = Atoms.t and
type elem = Atoms.t Var.pairvar
module BoolIntervals : BoolVar.S with
type s = Intervals.t and
type elem = Intervals.t Var.pairvar
module BoolChars : BoolVar.S with
type s = Chars.t and
type elem = Chars.t Var.pairvar
module BoolAbstracts: BoolVar.S with
type s = Abstracts.t and
type elem = Abstracts.t Var.pairvar
include Custom.T
module Node : Custom.T
......@@ -140,7 +141,7 @@ val record : label -> Node.t -> t
val record_fields : bool * Node.t label_map -> t
val char : Chars.t -> t
val constant : const -> t
val abstract : Abstract.t -> t
val abstract : Abstracts.t -> t
(** Helpers *)
......@@ -154,8 +155,7 @@ val empty_open_record: t
(** Positive systems and least solutions **)
module Positive :
sig
module Positive : sig
type v
val forward: unit -> v
val define: v -> v -> unit
......@@ -303,7 +303,14 @@ module Char : sig
val any : t
end
val get_abstract: t -> Abstract.t
module Abstract : sig
val has_abstract : t -> Abstracts.T.t -> bool
val get: t -> BoolAbstracts.t
val any : t
end
(*
val get_abstract: t -> Abstracts.t
*)
val normalize : t -> 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