Bisect report

000001| open QCheck

000002| open LCheck

000003|

000004| module Label =

000005| struct

000006| type elem = int

000007| let arb_elem = (*[1]*)Arbitrary.(choose [int 8; small_int]) (*was:Arbitrary.int 1000000*) (*max_int 4611686018427387903*)

000008| let to_string = (*[1]*)string_of_int

000009| end

000010| module Labellist = MkArbListArg(Label)

000011|

000012| module Str_arg =

000013| struct

000014| type elem = string

000015| let to_string s = (*[0]*)s

000016| let arb_elem = (*[1]*)Arbitrary.(choose [among ["a";"b";"c";"d";"e"]; string]) (* was: Arbitrary.string *)

000017| end

000018| module Strlist = MkArbListArg(Str_arg)

000019|

000020| (** Generic operations for building arbitrary sets *)

000021|

000022| (* build_set : 'a Set.t -> ('a -> 'a Set.t) -> ('a Set.t -> 'a Set.t -> 'a Set.t)

000023| -> 'a list -> 'a Set.t Arbitrary.t *)

000024| let rec build_set mt sglton union ls = match ls with

000025| | [] -> (*[50983703]*)Arbitrary.return mt

000026| | [l] -> (*[50719998]*)Arbitrary.return (sglton l)

000027| | _ -> (*[82574862]*)Arbitrary.(int (1 + List.length ls) >>= fun i ->

000028| (*[82574862]*)let ls,rs = split i ls in

000029| (*[82574862]*)lift2 union

000030| (build_set mt sglton union ls)

000031| (build_set mt sglton union rs) )

000032|

000033| (* build_map : ('b Map.t) -> ('a -> 'b -> 'b Map.t -> 'b Map.t) -> 'a * 'b list -> 'b Map.t *)

000034| let build_map mt add ls =

000035| (*[7243947]*)List.fold_right (fun (k,v) acctbl -> (*[66270545]*)add k v acctbl) ls mt

000036|

000037| (* permute : 'a list -> 'a list Arbitrary.t *)

000038| let rec permute es = match es with

000039| | [] -> (*[1050946]*)Arbitrary.return []

000040| | [e] -> (*[29520151]*)Arbitrary.return [e]

000041| | _ ->

000042| (*[18177624]*)let len = List.length es in

000043| (*[18177624]*)let front,back = split (len/2) es in

000044| (*[18177624]*)Arbitrary.(permute front >>= fun front' ->

000045| (*[17753858]*)permute back >>= fun back' ->

000046| (*[17753858]*)Arbitrary.bool >>= fun b ->

000047| (*[17753858]*)if b then (*[8878559]*)return (front' @ back') else (*[8875299]*)return (back' @ front'))

000048|

000049| (* le_gen : 'a list -> ('a list -> 'b) -> 'b *)

000050| let le_gen es build =

000051| (*[12284321]*)let es_gen = permute es in

000052| (*[12284321]*)Arbitrary.(es_gen >>= fun es ->

000053| (*[11874571]*)int (1 + List.length es) >>= fun i ->

000054| (*[11874571]*)let smaller_es,_ = split i es in

000055| (*[11874571]*)build smaller_es)

000056|

000057| (* le_entries : ('b -> 'b Arb.t) -> ('a * 'b) list -> (('a * 'b) list) Arb.t *)

000058| let le_entries arb_elem_le es =

000059| (*[548942]*)let rec build es = match es with

000060| | [] -> (*[548942]*)Arbitrary.return []

000061| | (k,v)::es -> (*[2794921]*)Arbitrary.(build es >>= fun es' ->

000062| (*[2794921]*)arb_elem_le v >>= fun v' ->

000063| (*[2794921]*)return ((k,v')::es')) in

000064| (*[548942]*)build es

000065|

000066| (* lift5 : ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a t -> 'b t -> 'c t -> 'd t -> 'e t -> 'f t *)

000067| let lift5 f gen_a gen_b gen_c gen_d gen_e =

000068| (*[10184134]*)Arbitrary.(gen_a >>= fun a ->

000069| (*[85401289]*)gen_b >>= fun b ->

000070| (*[85401289]*)gen_c >>= fun c ->

000071| (*[85401289]*)gen_d >>= fun d ->

000072| (*[85401289]*)gen_e >>= fun e -> (*[85401289]*)return (f a b c d e))

000073|

000074| (** Absence lattice extended with generators *)

000075| module Abs = struct

000076| let name = (*[1]*)"absence lattice"

000077| include Absencelattice

000078| let arb_elem = (*[1]*)Arbitrary.among [bot; top]

000079| let equiv_pair = (*[1]*)Arbitrary.(lift (fun a -> ((*[2000]*)a,a)) arb_elem)

000080| let arb_elem_le e = (*[2297387]*)if e = top then (*[757860]*)arb_elem else (*[1539527]*)Arbitrary.return bot

000081| end

000082|

000083| (** Number lattice extended with generators *)

000084| module Num = struct

000085| let name = (*[1]*)"number lattice"

000086| include Numberlattice

000087| let arb_elem = (*[1]*)Arbitrary.among [bot; top]

000088| let equiv_pair = (*[1]*)Arbitrary.(lift (fun a -> ((*[142458]*)a,a)) arb_elem)

000089| let arb_elem_le e = (*[3870973]*)if e = top then (*[1915513]*)arb_elem else (*[1955460]*)Arbitrary.return bot

000090| end

000091|

000092| (** String lattice extended with generators *)

000093| module Str = struct

000094| let name = (*[1]*)"string lattice"

000095| include Stringlattice

000096| let arb_elem = (*[1]*)Arbitrary.(choose [return bot; lift const Str_arg.arb_elem; return top])

000097| let equiv_pair = (*[1]*)Arbitrary.(lift (fun sv -> match sv with

000098| | Const s -> ((*[49292]*)sv,Const (String.copy s))

000099| | _ -> ((*[99166]*)sv,sv)) arb_elem)

000100| let arb_elem_le e = match e with

000101| | Bot -> (*[1613881]*)Arbitrary.return bot

000102| | Const s -> (*[1137747]*)Arbitrary.among [bot; Const s]

000103| | Top -> (*[1125345]*)arb_elem

000104| end

000105|

000106| (** Value lattice extended with generators *)

000107| module VL = struct

000108| let name = (*[1]*)"value lattice"

000109| let arb_num = (*[1]*)Num.arb_elem (* shorthands for the extended Num operations: *)

000110| let num_equiv_pair = (*[1]*)Num.equiv_pair (* Moving them below 'include' will shadow Num *)

000111| let num_arb_elem_le = (*[1]*)Num.arb_elem_le

000112|

000113| let arb_str = (*[1]*)Str.arb_elem (* shorthands for the extended Str operations: *)

000114| let str_equiv_pair = (*[1]*)Str.equiv_pair (* Moving them below 'include' will shadow Str *)

000115| let str_arb_elem_le = (*[1]*)Str.arb_elem_le

000116|

000117| include Valuelattice

000118| (* various helper functions *)

000119| let arb_tag t = (*[3]*)Arbitrary.(among [TagSet.singleton t; TagSet.empty])

000120| let arb_tags = (*[1]*)Arbitrary.(lift3

000121| (fun nl bl ud -> (*[75198624]*)TagSet.union (TagSet.union nl bl) ud)

000122| (arb_tag Nil) (arb_tag Bool) (arb_tag Userdata))

000123| let arb_builtin = (*[1]*)Arbitrary.(lift (fun b -> (*[95048575]*)Builtin b)

000124| (among [Error;Next;Pairs;Print;Write;Tonumber;Tostring;Abs;Ceil;Floor;

000125| Mod;Strlen;Strupper;Strlower;Strchar;Strbyte;Strsub;Sqrt;Type;Format;

000126| Getmetatable;Setmetatable]))

000127| let arb_funtag = (*[1]*)Arbitrary.(lift (fun i -> (*[95066035]*)Funtag i) Label.arb_elem)

000128| let arb_proc = (*[1]*)Arbitrary.(choose [arb_funtag; arb_builtin])

000129| let arb_procs = (*[1]*)Arbitrary.(fix ~max:5 ~base:(return ProcSet.empty) (lift2 ProcSet.add arb_proc))

000130| let arb_labels = (*[1]*)Arbitrary.(fix ~max:5 ~base:(return LabelSet.empty) (lift2 LabelSet.add Label.arb_elem))

000131|

000132| let arb_label_list = (*[1]*)Labellist.arb_elem

000133| let arb_tag_list = (*[1]*)Arbitrary.(list ~len:(int 4) (among [Nil; Bool; Userdata]))

000134| let arb_proc_list = (*[1]*)Arbitrary.(list ~len:(int 20) arb_proc)

000135|

000136| let build_labelset = (*[1]*)build_set LabelSet.empty LabelSet.singleton LabelSet.union

000137| let build_tagset = (*[1]*)build_set TagSet.empty TagSet.singleton TagSet.union

000138| let build_procset = (*[1]*)build_set ProcSet.empty ProcSet.singleton ProcSet.union

000139|

000140| (* arb_elem : elem Arbitrary.t *)

000141| let arb_elem = (* generate arbitrary tagset, number elem, string elem, fun set, table set *)

000142| (*[1]*)lift5 (fun tags num s procs labels ->

000143| (*[75198624]*){ tags = tags;

000144| number = num;

000145| strings = s;

000146| funs = procs;

000147| tables = labels }) arb_tags arb_num arb_str arb_procs arb_labels

000148|

000149| (* equiv_pair : (elem * elem) Arbitrary.t *)

000150| let equiv_pair =

000151| (*[1]*)let equiv_labelsets = Arbitrary.(arb_label_list >>= fun ls -> (*[141458]*)pair (build_labelset ls) (build_labelset ls)) in

000152| (*[1]*)let equiv_tagsets = Arbitrary.(arb_tag_list >>= fun ts -> (*[141458]*)pair (build_tagset ts) (build_tagset ts)) in

000153| (*[1]*)let equiv_procsets = Arbitrary.(arb_proc_list >>= fun ps -> (*[141458]*)pair (build_procset ps) (build_procset ps)) in

000154| (*[1]*)lift5 (fun (t,t') (n,n') (s,s') (p,p') (l,l') ->

000155| ((*[141458]*){ tags = t; number = n; strings = s; funs = p; tables = l },

000156| { tags = t'; number = n'; strings = s'; funs = p'; tables = l' }))

000157| equiv_tagsets num_equiv_pair str_equiv_pair equiv_procsets equiv_labelsets

000158|

000159| (* arb_elem_le : elem -> elem Arbitrary.t *)

000160| let arb_elem_le e =

000161| (*[3861973]*)let le_num_gen = num_arb_elem_le e.number in

000162| (*[3861973]*)let le_str_gen = str_arb_elem_le e.strings in

000163| (*[3861973]*)let le_tag_gen = le_gen (TagSet.elements e.tags) build_tagset in

000164| (*[3861973]*)let le_proc_gen = le_gen (ProcSet.elements e.funs) build_procset in

000165| (*[3861973]*)let le_label_gen = le_gen (LabelSet.elements e.tables) build_labelset in

000166| (*[3861973]*)lift5 (fun t n s p l -> (*[3739048]*){ tags = t; number = n; strings = s; funs = p; tables = l })

000167| le_tag_gen le_num_gen le_str_gen le_proc_gen le_label_gen

000168| end

000169|

000170| (** Environment lattice extended with generators *)

000171| module EL = struct

000172| let name = (*[1]*)"environment lattice"

000173| include Envlattice

000174| (* Helpers *)

000175| let arb_env_pair = (*[1]*)Arbitrary.(pair Label.arb_elem (list ~len:(int_range ~start:1 ~stop:10) Label.arb_elem))

000176| let arb_env_list = (*[1]*)Arbitrary.(list ~len:(int_range ~start:1 ~stop:10) arb_env_pair)

000177| let build_envset es = (*[725302]*)build_set PairSet.empty PairSet.singleton PairSet.union es

000178| (* Actual operations *)

000179| let arb_elem = (*[1]*)Arbitrary.(arb_env_list >>= build_envset)

000180| let equiv_pair = (*[1]*)Arbitrary.(arb_env_list >>= fun es -> (*[44000]*)pair (build_envset es) (build_envset es))

000181| let arb_elem_le e = (*[108485]*)le_gen (PairSet.elements e) build_envset

000182| end

000183|

000184| (** Property lattice extended with generators *)

000185| module PL = struct

000186| let name = (*[1]*)"property lattice"

000187| let abs_arb_elem = (*[1]*)Abs.arb_elem

000188| let abs_arb_elem_le = (*[1]*)Abs.arb_elem_le

000189| let vl_arb_elem = (*[1]*)Arbitrary.map VL.arb_elem VL.exclude_nil

000190| let vl_equiv_pair = (*[1]*)VL.equiv_pair

000191| let vl_arb_elem_le e = (*[3642683]*)Arbitrary.map (VL.arb_elem_le e) VL.exclude_nil

000192| include Proplattice

000193| let build_sc_set = (*[1]*)build_set ScopeChainSet.empty ScopeChainSet.singleton ScopeChainSet.union

000194| let build_tblmap = (*[1]*)build_map TableMap.empty TableMap.add

000195| let arb_sc_list = (*[1]*)Arbitrary.(list ~len:(int_range ~start:1 ~stop:10) (list ~len:(int_range ~start:1 ~stop:10) Label.arb_elem))

000196| let arb_key = (*[1]*)Arbitrary.(small_int >>= fun i ->

000197| (*[56151432]*)if i > 90

000198| then (*[5055465]*)return TableKey.Metatable

000199| else (*[51095967]*)lift (fun s -> (*[51095967]*)TableKey.String s) Str_arg.arb_elem)

000200| let arb_entries = (*[1]*)Arbitrary.(list ~len:(int 20) (pair arb_key

000201| (pair vl_arb_elem abs_arb_elem)))

000202| let coll_defs es =

000203| (*[0]*)List.fold_left (fun (kacc,vacc) (k,(v,_abs)) -> match k with

000204| | TableKey.String k -> ((*[0]*)VL.join (VL.string k) kacc, VL.join v vacc)

000205| | TableKey.Metatable -> ((*[0]*)kacc,vacc)) (VL.bot,VL.bot) es

000206|

000207| let arb_elem =

000208| (*[1]*)let sc_gen = Arbitrary.(arb_sc_list >>= build_sc_set) in

000209| (*[1]*)let table_gen = Arbitrary.map arb_entries build_tblmap in

000210| (*[1]*)let vl_arb_key = Arbitrary.map vl_arb_elem VL.exclude_strings in

000211|

000212| (*[1]*)Arbitrary.(small_int >>= fun i ->

000213| (*[6475400]*)if i > 90

000214| then (*[582184]*)return bot

000215| else

000216| (*[5893216]*)lift5

000217| (fun t ds dk df sc ->

000218| (*[5893216]*)table { table = t;

000219| default_str = ds;

000220| default_key = dk;

000221| default = df;

000222| scopechain = sc })

000223| table_gen vl_arb_elem vl_arb_key vl_arb_elem sc_gen)

000224|

000225| let equiv_pair =

000226| (*[1]*)let vl_equiv_pair_nonnil = Arbitrary.(vl_equiv_pair >>= fun (v,v') -> (*[30972]*)return (VL.exclude_nil v,

000227| VL.exclude_nil v')) in

000228| (*[1]*)let equiv_keys = Arbitrary.(vl_equiv_pair >>= fun (v,v') -> (*[15486]*)return (VL.exclude_strings v,

000229| VL.exclude_strings v')) in

000230| (*[1]*)let equiv_tables = Arbitrary.(map arb_entries build_tblmap >>= fun map ->

000231| (*[15486]*)permute (TableMap.bindings map) >>= fun perm_entries ->

000232| (*[15486]*)return (map, build_tblmap perm_entries)) in

000233| (*[1]*)let equiv_scopechains = Arbitrary.(arb_sc_list >>= fun sc -> (*[15486]*)pair (build_sc_set sc)

000234| (build_sc_set sc)) in

000235| (*[1]*)Arbitrary.(small_int >>= fun i ->

000236| (*[17000]*)if i > 90

000237| then (*[1514]*)return (bot,bot)

000238| else

000239| (*[15486]*)lift5

000240| (fun (t,t') (ds,ds') (dk,dk') (df,df') (sc,sc') ->

000241| ((*[15486]*)Table { table = t; default_str = ds; default_key = dk; default = df; scopechain = sc },

000242| Table { table = t'; default_str = ds'; default_key = dk'; default = df'; scopechain = sc' }))

000243| equiv_tables vl_equiv_pair_nonnil equiv_keys vl_equiv_pair_nonnil equiv_scopechains)

000244|

000245| (* prop_le_gen : 'a list -> ('a list -> 'b) -> 'b *)

000246| let prop_le_gen es build blddefkey blddef =

000247| (*[0]*)let es_gen = permute es in

000248| (*[0]*)Arbitrary.(es_gen >>= fun es ->

000249| (*[0]*)int (1 + List.length es) >>= fun i ->

000250| (*[0]*)let smaller_es,rest_es = split i es in

000251| (*[0]*)let collk,collv =

000252| List.fold_left (fun (kacc,vacc) (k,(v,_abs)) -> match k with

000253| | TableKey.String k -> ((*[0]*)VL.join (VL.string k) kacc, VL.join v vacc)

000254| | TableKey.Metatable -> ((*[0]*)kacc,vacc)) (VL.bot,VL.bot) rest_es in

000255| (*[0]*)Arbitrary.triple (build smaller_es) (blddefkey collk) (blddef collv)

000256| )

000257|

000258| (* pl_le_gen : 'a list -> ('a list -> 'b) -> 'b *)

000259| let pl_le_gen es build =

000260| (*[454432]*)let es_gen = permute es in

000261| (*[454432]*)Arbitrary.(es_gen >>= fun es ->

000262| (*[413457]*)let uncert,cert = List.partition (fun (k,(v,a)) -> (*[3031981]*)a = Abs.maybe_absent) es in

000263| (*[413457]*)int (1 + List.length uncert) >>= fun i ->

000264| (*[413457]*)let smaller_uc,_ = split i uncert in

000265| (*[413457]*)build (smaller_uc@cert))

000266|

000267| let arb_elem_le t = match t with

000268| | Bot -> (*[45617]*)Arbitrary.return bot

000269| | Table { table = tbl; default_str; default_key; default; scopechain } ->

000270| (*[454432]*)let entry_le (v,a) =

000271| (*[2279387]*)Arbitrary.(pair (vl_arb_elem_le v) (abs_arb_elem_le a) >>= (fun (v',a') ->

000272| (*[2279387]*)if (*[2279387]*)VL.is_bot v' && (*[68256]*)a' = Abs.is_present

000273| then (*[57595]*)return (v,a') (* don't generate bottom, certain entries *)

000274| else (*[2221792]*)return (v',a'))) in

000275| (*[454432]*)let table' = pl_le_gen (TableMap.bindings tbl)

000276| Arbitrary.(fun es -> (*[413457]*)map (le_entries entry_le es) build_tblmap) in

000277| (*[454432]*)let vl_arb_key_le e = (*[908864]*)vl_arb_elem_le e in

000278| (*[454432]*)let def_str' = vl_arb_key_le default_str in

000279| (*[454432]*)let def_key' = vl_arb_key_le default_key in

000280| (*[454432]*)let default' = vl_arb_elem_le default in

000281| (*[454432]*)let scopechain' = le_gen (ScopeChainSet.elements scopechain) build_sc_set in

000282|

000283| (* definite bindings in arg. *cannot* be deleted in generated smaller table *)

000284| (* uncertain bindings in arg. *can* be deleted in generated smaller table *)

000285| (* bindings can be added to the generated smaller table

000286| -- if the bigger table default accounts for them *)

000287| (*[454432]*)let coll_removed_entries es candtab canddefstr = (* collects smaller defs *)

000288| (*[413457]*)List.fold_left (fun acc (k,(v,_abs)) -> match k with

000289| | TableKey.String k' ->

000290| (*[2813778]*)if TableMap.mem k candtab (* entry present, and smaller value generated *)

000291| then (*[2115295]*)acc

000292| else (*[698483]*)VL.meet v acc (* entry not present, so default should be less *)

000293| | TableKey.Metatable -> (*[218203]*)acc) canddefstr es in

000294|

000295| (*[454432]*)Arbitrary.(small_int >>= fun i ->

000296| (*[454432]*)if i > 90

000297| then (*[40975]*)return bot

000298| else

000299| (*[413457]*)let bindings = TableMap.bindings tbl in

000300| (*[413457]*)lift5

000301| (fun t ds dk df sc ->

000302| (* ensure that collective default does not increase above removed entries *)

000303| (*[413457]*)let new_defstr = coll_removed_entries bindings t ds in

000304| (*[413457]*)table {table = t;

000305| default_str = new_defstr;

000306| default_key = dk;

000307| default = df;

000308| scopechain = sc})

000309| table' def_str' def_key' default' scopechain')

000310| end

000311|

000312| (** Store lattice extended with generators *)

000313| module ST = struct

000314| let name = (*[1]*)"store lattice"

000315| let pl_arb_elem = (*[1]*)PL.arb_elem

000316| let pl_arb_elem_le = (*[1]*)PL.arb_elem_le

000317| include Storelattice

000318| let build_storemap = (*[1]*)build_map StoreMap.empty StoreMap.add

000319| let arb_entries = (*[1]*)Arbitrary.(list ~len:(int 20) (pair Label.arb_elem pl_arb_elem))

000320| let arb_elem = (*[1]*)Arbitrary.map arb_entries build_storemap

000321| let equiv_pair = (*[1]*)Arbitrary.(map arb_entries build_storemap >>= fun map ->

000322| (*[60000]*)permute (StoreMap.bindings map) >>= fun perm_entries ->

000323| (*[60000]*)return (map, build_storemap perm_entries))

000324| let arb_elem_le st = (*[124485]*)le_gen (StoreMap.bindings st)

000325| Arbitrary.(fun es -> (*[124485]*)map (le_entries pl_arb_elem_le es) build_storemap)

000326| end

000327|

000328| (** State lattice extended with generators *)

000329| module SL = struct

000330| let name = (*[1]*)"state lattice"

000331| let st_arb_elem = (*[1]*)ST.arb_elem

000332| let st_equiv_pair = (*[1]*)ST.equiv_pair

000333| let st_arb_elem_le = (*[1]*)ST.arb_elem_le

000334| let el_arb_elem = (*[1]*)EL.arb_elem

000335| let el_equiv_pair = (*[1]*)EL.equiv_pair

000336| let el_arb_elem_le = (*[1]*)EL.arb_elem_le

000337| include Statelattice

000338| let arb_elem = (*[1]*)Arbitrary.lift2 (fun st e -> (*[499817]*){ store = st; env = e }) st_arb_elem el_arb_elem

000339| let equiv_pair = (*[1]*)Arbitrary.lift2

000340| (fun (st,st') (e,e') -> ((*[40000]*){ store = st; env = e },

000341| { store = st'; env = e' })) st_equiv_pair el_equiv_pair

000342| let arb_elem_le { store; env } =

000343| (*[96485]*)Arbitrary.lift2 (fun st e -> (*[96485]*){ store = st; env = e }) (st_arb_elem_le store) (el_arb_elem_le env)

000344| end

000345|

000346| (** Analysis lattice extended with generators *)

000347| module AL = struct

000348| let name = (*[1]*)"analysis lattice"

000349| let sl_arb_elem = (*[1]*)SL.arb_elem

000350| let sl_arb_elem_le = (*[1]*)SL.arb_elem_le

000351| include Analysislattice

000352| let build_labelmap = (*[1]*)build_map LabelMap.empty LabelMap.add

000353| let arb_entries = (*[1]*)Arbitrary.(list ~len:(int 20) (pair Label.arb_elem sl_arb_elem))

000354| let arb_elem = (*[1]*)Arbitrary.map arb_entries build_labelmap

000355| let equiv_pair = (*[1]*)Arbitrary.(map arb_entries build_labelmap >>= fun map ->

000356| (*[3000]*)permute (LabelMap.bindings map) >>= fun perm_entries ->

000357| (*[3000]*)return (map, build_labelmap perm_entries))

000358| let arb_elem_le st = (*[11000]*)le_gen (LabelMap.bindings st)

000359| Arbitrary.(fun es -> (*[11000]*)map (le_entries sl_arb_elem_le es) build_labelmap)

000360| end

000361|

000362| module GenAbsTests = GenericTests(Abs)

000363| module GenNumTests = GenericTests(Num)

000364| module GenStrTests = GenericTests(Str)

000365| module GenValTests = GenericTests(VL)

000366| module GenEnvTests = GenericTests(EL)

000367| module GenPropTests = GenericTests(PL)

000368| module GenStoTests = GenericTests(ST)

000369| module GenStaTests = GenericTests(SL)

000370| module GenAnaTests = GenericTests(AL)

000371|

000372| module GenAbsTopTests = GenericTopTests(Abs)

000373| module GenNumTopTests = GenericTopTests(Num)

000374| module GenStrTopTests = GenericTopTests(Str)

000375|

000376|

000377| (** Tests for specific operations *)

000378|

000379| module VLAbsPair = MkPairLattice(VL)(Abs)

000380| module GenVLAbspairTests = GenericTests(VLAbsPair)

000381|

000382| module VLVLpair = MkPairLattice(VL)(VL)

000383| module GenVLVLpairTests = GenericTests(VLVLpair)

000384|

000385| module VLlist = MkListLattice(VL)

000386| module GenVLlistTests = GenericTests(VLlist)

000387|

000388| module SLVLlistpair = MkPairLattice(SL)(VLlist)

000389| module GenSLVLlistpairTests = GenericTests(SLVLlistpair)

000390|

000391|

000392| (** String lattice *)

000393|

000394| (* Note: the following predicate functions depend on the Boolean lattice: *)

000395| (* {true,false} under reverse implication ordering, *)

000396| (* bot = true <== true <== false <== false = top *)

000397| let empty_tests =

000398| (*[1]*)let str_empty = ("Str.empty",Str.empty) in

000399| [ (*[1]*)testsig (module Str) -$-> (module Bool) =: str_empty;

000400| testsig (module Str) -<-> (module Bool) =: str_empty;

000401| testsig (module Str) -~-> (module Bool) =: str_empty; ]

000402|

000403| (* Note: the following predicate functions depend on the Boolean lattice: *)

000404| (* {true,false} under implication ordering, *)

000405| (* bot = false <== false <== true <== true = top *)

000406| let nonempty_tests =

000407| (*[1]*)let str_nonempty = ("Str.nonempty",Str.nonempty) in

000408| [ (*[1]*)testsig (module Str) -$-> (module DBool) =: str_nonempty;

000409| testsig (module Str) -<-> (module DBool) =: str_nonempty;

000410| testsig (module Str) -~-> (module DBool) =: str_nonempty; ]

000411|

000412| let upper_tests =

000413| (*[1]*)let str_upper = ("Str.upper",Str.upper) in

000414| [ (*[1]*)testsig (module Str) -$-> (module Str) =: str_upper;

000415| testsig (module Str) -<-> (module Str) =: str_upper;

000416| testsig (module Str) -~-> (module Str) =: str_upper; ]

000417|

000418| let lower_tests =

000419| (*[1]*)let str_lower = ("Str.lower",Str.lower) in

000420| [ (*[1]*)testsig (module Str) -$-> (module Str) =: str_lower;

000421| testsig (module Str) -<-> (module Str) =: str_lower;

000422| testsig (module Str) -~-> (module Str) =: str_lower; ]

000423|

000424| let concat_tests =

000425| (*[1]*)let str_concat = ("Str.concat",Str.concat) in

000426| [ (*[1]*)testsig (module Str) -$-> (module Str) ---> (module Str) =: str_concat;

000427| testsig (module Str) ---> (module Str) -$-> (module Str) =: str_concat;

000428| testsig (module Str) -<-> (module Str) ---> (module Str) =: str_concat;

000429| testsig (module Str) ---> (module Str) -<-> (module Str) =: str_concat;

000430| testsig (module Str) -~-> (module Str) ---> (module Str) =: str_concat;

000431| testsig (module Str) ---> (module Str) -~-> (module Str) =: str_concat; ]

000432|

000433| let concat_sound = (* forall s,s'. abs(s ^ s') = abs(s) ^ abs(s') *)

000434| (*[1]*)let pp_pair = PP.pair (fun i -> (*[0]*)i) (fun i -> (*[0]*)i) in

000435| (*[1]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("Str.concat sound") ~size:(fun p -> (*[0]*)String.length (pp_pair p))

000436| Arbitrary.(pair string string)

000437| (fun (s,s') -> (*[1000]*)Str.(eq (concat (const s) (const s')) (const (s ^ s')) ))

000438|

000439| (* test suite for specific string operations *)

000440| let spec_str_operations =

000441| (*[1]*)flatten

000442| [ empty_tests;

000443| nonempty_tests;

000444| upper_tests;

000445| lower_tests;

000446| concat_tests;

000447| [concat_sound] ]

000448|

000449|

000450| (** Value lattice *)

000451|

000452| (* generic combinators for checking properties of unary queries *)

000453|

000454| (* Note: the following predicate functions depend on the Boolean lattice: *)

000455| (* {true,false} under implication ordering, *)

000456| (* bot = false <== false <== true <== true = top *)

000457| let query_monotone_invariant_dbool qname q =

000458| (*[6]*)let vl_pair = (qname,q) in

000459| [(*testsig (module VL) -$-> (module DBool) =: vl_pair;*)

000460| (*[6]*)testsig (module VL) -<-> (module DBool) =: vl_pair;

000461| testsig (module VL) -~-> (module DBool) =: vl_pair; ]

000462|

000463| (* Note: the following predicate functions depend on the Boolean lattice: *)

000464| (* {true,false} under reverse implication ordering, *)

000465| (* bot = true <== true <== false <== false = top *)

000466| let query_strict_monotone_invariant_bool qname q =

000467| (*[4]*)let vl_pair = (qname,q) in

000468| [(*[4]*)testsig (module VL) -$-> (module Bool) =: vl_pair;

000469| testsig (module VL) -<-> (module Bool) =: vl_pair;

000470| testsig (module VL) -~-> (module Bool) =: vl_pair; ]

000471|

000472| let unary_is_strict_monotone_invariant name op =

000473| (*[14]*)let vl_pair = (name,op) in

000474| [ (*[14]*)testsig (module VL) -$-> (module VL) =: vl_pair;

000475| testsig (module VL) -<-> (module VL) =: vl_pair;

000476| testsig (module VL) -~-> (module VL) =: vl_pair; ]

000477|

000478| let binop_is_strict_monotone_invariant name op =

000479| (*[14]*)let vl_pair = (name,op) in

000480| [ (*[14]*)testsig (module VL) -$-> (module VL) ---> (module VL) =: vl_pair;

000481| testsig (module VL) ---> (module VL) -$-> (module VL) =: vl_pair;

000482| testsig (module VL) -<-> (module VL) ---> (module VL) =: vl_pair;

000483| testsig (module VL) ---> (module VL) -<-> (module VL) =: vl_pair;

000484| testsig (module VL) -~-> (module VL) ---> (module VL) =: vl_pair;

000485| testsig (module VL) ---> (module VL) -~-> (module VL) =: vl_pair; ]

000486|

000487| (* test suite for specific value operations *)

000488| let spec_vl_operations =

000489| (*[1]*)flatten

000490| [ (* unary op tests *)

000491| unary_is_strict_monotone_invariant "VL.exclude_nil" VL.exclude_nil;

000492| unary_is_strict_monotone_invariant "VL.exclude_strings" VL.exclude_strings;

000493| unary_is_strict_monotone_invariant "VL.exclude_proc" VL.exclude_proc;

000494| unary_is_strict_monotone_invariant "VL.exclude_tables" VL.exclude_tables;

000495| unary_is_strict_monotone_invariant "VL.only_tables" VL.only_tables;

000496| unary_is_strict_monotone_invariant "VL.coerce_tonum" VL.coerce_tonum;

000497| unary_is_strict_monotone_invariant "VL.coerce_tostring" VL.coerce_tostring;

000498| unary_is_strict_monotone_invariant "VL.upper" VL.upper;

000499| unary_is_strict_monotone_invariant "VL.lower" VL.lower;

000500| unary_is_strict_monotone_invariant "VL.char" VL.char;

000501| unary_is_strict_monotone_invariant "VL.typep" VL.typep;

000502| unary_is_strict_monotone_invariant "VL.unop Ast.Uminus" (VL.unop Ast.Uminus);

000503| unary_is_strict_monotone_invariant "VL.unop Ast.Length" (VL.unop Ast.Length);

000504| unary_is_strict_monotone_invariant "VL.unop Ast.Not" (VL.unop Ast.Not);

000505| (* binop tests *)

000506| binop_is_strict_monotone_invariant "VL.or_join" VL.or_join;

000507| binop_is_strict_monotone_invariant "VL.binop Ast.Eq" (VL.binop Ast.Eq);

000508| binop_is_strict_monotone_invariant "VL.binop Ast.Lt" (VL.binop Ast.Lt);

000509| binop_is_strict_monotone_invariant "VL.binop Ast.Gt" (VL.binop Ast.Gt);

000510| binop_is_strict_monotone_invariant "VL.binop Ast.Ne" (VL.binop Ast.Ne);

000511| binop_is_strict_monotone_invariant "VL.binop Ast.Le" (VL.binop Ast.Le);

000512| binop_is_strict_monotone_invariant "VL.binop Ast.Ge" (VL.binop Ast.Ge);

000513| binop_is_strict_monotone_invariant "VL.binop Ast.Plus" (VL.binop Ast.Plus);

000514| binop_is_strict_monotone_invariant "VL.binop Ast.Minus" (VL.binop Ast.Minus);

000515| binop_is_strict_monotone_invariant "VL.binop Ast.Times" (VL.binop Ast.Times);

000516| binop_is_strict_monotone_invariant "VL.binop Ast.Div" (VL.binop Ast.Div);

000517| binop_is_strict_monotone_invariant "VL.binop Ast.Mod" (VL.binop Ast.Mod);

000518| binop_is_strict_monotone_invariant "VL.binop Ast.Pow" (VL.binop Ast.Pow);

000519| binop_is_strict_monotone_invariant "VL.binop Ast.Concat" (VL.binop Ast.Concat);

000520| (* query tests (under reverse implication ordering) *)

000521| query_strict_monotone_invariant_bool "is_bot" VL.is_bot;

000522| query_strict_monotone_invariant_bool "is_nil" VL.is_nil;

000523| query_strict_monotone_invariant_bool "is_number" VL.is_number;

000524| query_strict_monotone_invariant_bool "is_strings" VL.is_strings;

000525| (* query tests (under implication ordering) *)

000526| query_monotone_invariant_dbool "may_be_nil" VL.may_be_nil;

000527| query_monotone_invariant_dbool "may_be_non_nil" VL.may_be_non_nil;

000528| query_monotone_invariant_dbool "may_be_number" VL.may_be_number;

000529| query_monotone_invariant_dbool "may_be_non_strings" VL.may_be_non_strings;

000530| query_monotone_invariant_dbool "may_be_proc" VL.may_be_proc;

000531| query_monotone_invariant_dbool "may_be_table" VL.may_be_proc; ]

000532| (* The queries 'is_nil/is_number/is_strings' don't seem to exhibit lattice-based properties *)

000533| (* e.g., is_nil vlat = VL.leq vlat VL.nil

000534| is true at bot, and VL.nil but becomes false as the arg increases *)

000535|

000536|

000537| (** Environment lattice *)

000538|

000539| (* Note: the following predicate depends on the Boolean lattice *)

000540| (* {true,false} under reverse implication ordering. *)

000541| let is_bot_tests =

000542| (*[1]*)let el_is_bot = ("EL.is_bot",EL.is_bot) in

000543| [ (*[1]*)testsig (module EL) -$-> (module Bool) =: el_is_bot;

000544| testsig (module EL) -<-> (module Bool) =: el_is_bot;

000545| testsig (module EL) -~-> (module Bool) =: el_is_bot; ]

000546|

000547| let enter_scope_tests = (* enter_scope : EL -> label -> EL *)

000548| (*[1]*)let el_enter_scope = ("EL.enter_scope",EL.enter_scope) in

000549| [ (*[1]*)pw_right (module Label) op_strict (module EL) (module EL) =:: el_enter_scope;

000550| pw_right (module Label) op_monotone (module EL) (module EL) =:: el_enter_scope;

000551| pw_right (module Label) op_invariant (module EL) (module EL) =:: el_enter_scope; ]

000552|

000553| (* test suite for specific environment operations *)

000554| let spec_env_operations =

000555| (*[1]*)flatten [

000556| is_bot_tests;

000557| enter_scope_tests;

000558| ]

000559|

000560|

000561| (** Property lattice *)

000562|

000563| (* Note: the following predicate depends on the Boolean lattice *)

000564| (* {true,false} under reverse implication ordering. *)

000565| let is_bot_tests =

000566| (*[1]*)let pl_is_bot = ("PL.is_bot",PL.is_bot) in

000567| [ (*[1]*)testsig (module PL) -$-> (module Bool) =: pl_is_bot;

000568| testsig (module PL) -<-> (module Bool) =: pl_is_bot;

000569| testsig (module PL) -~-> (module Bool) =: pl_is_bot; ]

000570|

000571| let find_exn_tests = (* find_exn : string -> PL -> VL + Not_found *)

000572| (*[1]*)let find_exn' str map = (*[5000]*)try (*[5000]*)PL.find_exn str map with Not_found -> (*[4034]*)VLAbsPair.bot in (* wrap 'find_exn' (which may raise exception) *)

000573| (*[1]*)let pl_find_exn = ("PL.find_exn",find_exn') in

000574| [ (*[1]*)pw_left (module Str_arg) op_strict (module PL) (module VLAbsPair) =:: pl_find_exn;

000575| pw_left (module Str_arg) op_monotone (module PL) (module VLAbsPair) =:: pl_find_exn;

000576| pw_left (module Str_arg) op_invariant (module PL) (module VLAbsPair) =:: pl_find_exn; ]

000577|

000578| let find_fail = (* forall s. find s bot = VL.nil *)

000579| (*[1]*)mk_test ~n:1000 ~pp:PP.string ~limit:1 ~name:("find fail in " ^ PL.name) ~size:(fun s -> (*[0]*)String.length (PP.string s))

000580| Arbitrary.string (fun s -> (*[1000]*)VL.eq (PL.find s PL.mt) VL.nil)

000581|

000582| let find_tests = (* find : string -> PL -> VL *)

000583| (*[1]*)let pl_find = ("PL.find",PL.find) in

000584| [ (*[1]*)find_fail;

000585| pw_left (module Str_arg) op_strict (module PL) (module VL) =:: pl_find; (* not strict b/c default *)

000586| pw_left (module Str_arg) op_monotone (module PL) (module VL) =:: pl_find; (* not monotone b/c default *)

000587| pw_left (module Str_arg) op_invariant (module PL) (module VL) =:: pl_find; ]

000588|

000589| let find_nonstr_defaults_tests =

000590| (*[1]*)let pl_find_nonstr_defaults = ("PL.find_nonstr_defaults",PL.find_nonstr_defaults) in

000591| [ (*[1]*)testsig (module PL) -$-> (module VLVLpair) =: pl_find_nonstr_defaults;

000592| testsig (module PL) -<-> (module VLVLpair) =: pl_find_nonstr_defaults;

000593| testsig (module PL) -~-> (module VLVLpair) =: pl_find_nonstr_defaults; ]

000594|

000595| let find_all_keys_tests =

000596| (*[1]*)let pl_find_all_keys = ("PL.find_all_keys",PL.find_all_keys) in

000597| [ (*[1]*)testsig (module PL) -$-> (module VL) =: pl_find_all_keys;

000598| testsig (module PL) -<-> (module VL) =: pl_find_all_keys;

000599| testsig (module PL) -~-> (module VL) =: pl_find_all_keys; ]

000600|

000601| let find_all_tests =

000602| (*[1]*)let pl_find_all = ("PL.find_all",PL.find_all) in

000603| [ (*[1]*)testsig (module PL) -$-> (module VL) =: pl_find_all;

000604| testsig (module PL) -<-> (module VL) =: pl_find_all;

000605| testsig (module PL) -~-> (module VL) =: pl_find_all; ]

000606|

000607| let get_metatable_tests =

000608| (*[1]*)let pl_get_metatable = ("PL.get_metatable",PL.get_metatable) in

000609| [ (*[1]*)testsig (module PL) -$-> (module VL) =: pl_get_metatable;

000610| testsig (module PL) -<-> (module VL) =: pl_get_metatable; (* include nil, hence not strict and monotone *)

000611| testsig (module PL) -~-> (module VL) =: pl_get_metatable; ]

000612|

000613| let set_metatable_tests =

000614| (*[1]*)let pl_set_metatable = ("PL.set_metatable",PL.set_metatable) in

000615| [ (*[1]*)testsig (module VL) -$-> (module PL) ---> (module PL) =: pl_set_metatable;

000616| testsig (module VL) -<-> (module PL) ---> (module PL) =: pl_set_metatable;

000617| testsig (module VL) -~-> (module PL) ---> (module PL) =: pl_set_metatable;

000618| testsig (module VL) ---> (module PL) -$-> (module PL) =: pl_set_metatable;

000619| testsig (module VL) ---> (module PL) -<-> (module PL) =: pl_set_metatable;

000620| testsig (module VL) ---> (module PL) -~-> (module PL) =: pl_set_metatable; ]

000621|

000622| let set_metatable_absent_tests =

000623| (*[1]*)let pl_set_metatable_absent = ("PL.set_metatable_absent",PL.set_metatable_absent) in

000624| [ (*[1]*)testsig (module PL) -$-> (module PL) =: pl_set_metatable_absent;

000625| testsig (module PL) -<-> (module PL) =: pl_set_metatable_absent;

000626| testsig (module PL) -~-> (module PL) =: pl_set_metatable_absent; ]

000627|

000628| let get_metatable_set_metatable_extensive = (* forall v,p. v <= get_metatable (set_metatable v p) *)

000629| (*[1]*)let pp_pair = PP.pair VL.to_string PL.to_string in

000630| (*[1]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("PL.get_meta_table-PL.set_meta_table extensive")

000631| ~size:(fun p -> (*[0]*)String.length (pp_pair p))

000632| Arbitrary.(pair VL.arb_elem PL.arb_elem)

000633| (fun (v,p) -> (*[1000]*)PL.leq p PL.bot (* Not true for bottom p and non-bottom v *)

000634| || (*[904]*)VL.leq v (PL.get_metatable (PL.set_metatable v p)))

000635|

000636| let add_tests = (* add : string -> VL -> PL -> PL *)

000637| (*[1]*)let pl_add = ("PL.add",PL.add) in

000638| [(*[1]*)pw_left (module Str_arg) (pw_right (module PL) op_strict) (module VL) (module PL) =:: pl_add;

000639| pw_left (module Str_arg) (pw_right (module PL) op_monotone) (module VL) (module PL) =:: pl_add;

000640| pw_left (module Str_arg) (pw_right (module PL) op_invariant) (module VL) (module PL) =:: pl_add;

000641| pw_left (module Str_arg) (pw_left (module VL) op_strict) (module PL) (module PL) =:: pl_add;

000642| pw_left (module Str_arg) (pw_left (module VL) op_monotone) (module PL) (module PL) =:: pl_add;

000643| pw_left (module Str_arg) (pw_left (module VL) op_invariant) (module PL) (module PL) =:: pl_add; ]

000644|

000645| let add_local_tests = (* add_local : string -> VL -> PL -> PL *)

000646| (*[1]*)let pl_add_local = ("PL.add_local",PL.add_local) in

000647| [(*[1]*)pw_left (module Str_arg) (pw_right (module PL) op_strict) (module VL) (module PL) =:: pl_add_local;

000648| pw_left (module Str_arg) (pw_right (module PL) op_monotone) (module VL) (module PL) =:: pl_add_local;

000649| pw_left (module Str_arg) (pw_right (module PL) op_invariant) (module VL) (module PL) =:: pl_add_local;

000650| pw_left (module Str_arg) (pw_left (module VL) op_strict) (module PL) (module PL) =:: pl_add_local;

000651| pw_left (module Str_arg) (pw_left (module VL) op_monotone) (module PL) (module PL) =:: pl_add_local;

000652| pw_left (module Str_arg) (pw_left (module VL) op_invariant) (module PL) (module PL) =:: pl_add_local; ]

000653|

000654| let add_nonstr_default_tests =

000655| (*[1]*)let pl_add_nonstr_default = ("PL.add_nonstr_default",PL.add_nonstr_default) in

000656| [ (*[1]*)testsig (module VL) -$-> (module VL) ---> (module PL) ---> (module PL) =: pl_add_nonstr_default;

000657| testsig (module VL) -<-> (module VL) ---> (module PL) ---> (module PL) =: pl_add_nonstr_default;

000658| testsig (module VL) -~-> (module VL) ---> (module PL) ---> (module PL) =: pl_add_nonstr_default;

000659| testsig (module VL) ---> (module VL) -$-> (module PL) ---> (module PL) =: pl_add_nonstr_default;

000660| testsig (module VL) ---> (module VL) -<-> (module PL) ---> (module PL) =: pl_add_nonstr_default;

000661| testsig (module VL) ---> (module VL) -~-> (module PL) ---> (module PL) =: pl_add_nonstr_default;

000662| testsig (module VL) ---> (module VL) ---> (module PL) -$-> (module PL) =: pl_add_nonstr_default;

000663| testsig (module VL) ---> (module VL) ---> (module PL) -<-> (module PL) =: pl_add_nonstr_default;

000664| testsig (module VL) ---> (module VL) ---> (module PL) -~-> (module PL) =: pl_add_nonstr_default; ]

000665|

000666| let add_scopechain_tests = (* add_scopechain : PL -> label list -> PL *)

000667| (*[1]*)let pl_add_scopechain = ("PL.add_scopechain",PL.add_scopechain) in

000668| [ (*[1]*)pw_right (module Labellist) op_strict (module PL) (module PL) =:: pl_add_scopechain;

000669| pw_right (module Labellist) op_monotone (module PL) (module PL) =:: pl_add_scopechain;

000670| pw_right (module Labellist) op_invariant (module PL) (module PL) =:: pl_add_scopechain; ]

000671|

000672| let add_all_str_tests =

000673| (*[1]*)let pl_add_all_str = ("PL.add_all_str", PL.add_all_str) in

000674| [ (*[1]*)testsig (module VL) -$-> (module PL) ---> (module PL) =: pl_add_all_str;

000675| testsig (module VL) -<-> (module PL) ---> (module PL) =: pl_add_all_str;

000676| testsig (module VL) -~-> (module PL) ---> (module PL) =: pl_add_all_str;

000677| testsig (module VL) ---> (module PL) -$-> (module PL) =: pl_add_all_str;

000678| testsig (module VL) ---> (module PL) -<-> (module PL) =: pl_add_all_str;

000679| testsig (module VL) ---> (module PL) -~-> (module PL) =: pl_add_all_str; ]

000680|

000681| (* Current 'add_all_params' not strict in first/second args *)

000682| let add_all_params_tests = (* add_all_params : string list -> VL list -> PL -> PL *)

000683| (*[1]*)let pl_add_all_params = ("PL.add_all_params",PL.add_all_params) in

000684| [ (*[1]*)pw_left (module Strlist) (pw_left (module VLlist) op_strict) (module PL) (module PL) =:: pl_add_all_params;

000685| pw_left (module Strlist) (pw_left (module VLlist) op_monotone) (module PL) (module PL) =:: pl_add_all_params;

000686| pw_left (module Strlist) (pw_left (module VLlist) op_invariant) (module PL) (module PL) =:: pl_add_all_params; ]

000687|

000688| let find_add_extensive = (* forall s,v,p. v <= find s (add s v p) *)

000689| (*[1]*)let pp_triple = PP.triple PP.string VL.to_string PL.to_string in

000690| (*[1]*)mk_test ~n:1000 ~pp:pp_triple ~limit:1 ~name:("find-add extensive in " ^ PL.name)

000691| ~size:(fun t -> (*[0]*)String.length (pp_triple t))

000692| Arbitrary.(triple string VL.arb_elem PL.arb_elem)

000693| (fun (s,v,p) -> (*[1000]*)PL.leq p PL.bot (* does not hold for bottom p and non-bottom s, v *)

000694| || (*[909]*)VL.leq v (PL.find s (PL.add s v p)))

000695|

000696| let find_add_monotone = (* forall s,v,v',p. v <= v' ==> find s (add s v p) <= find s (add s v' p)*)

000697| (*[1]*)let pp_triple = PP.triple PP.string GenValTests.pp_pair PL.to_string in

000698| (*[1]*)mk_test ~n:1000 ~pp:pp_triple ~limit:1 ~name:("find-add monotone in " ^ PL.name)

000699| ~size:(fun t -> (*[0]*)String.length (pp_triple t))

000700| Arbitrary.(triple string GenValTests.ord_pair PL.arb_elem)

000701| (fun (s,(v,v'),p) -> (*[1000]*)Prop.assume (VL.leq v v');

000702| (*[1000]*)VL.leq (PL.find s (PL.add s v p)) (PL.find s (PL.add s v' p)))

000703|

000704| let find_exn_add_local_extensive = (* forall s,v,p. v <= find_exn s (add s v p) *)

000705| (*[1]*)let pp_triple = PP.triple PP.string VL.to_string PL.to_string in

000706| (*[1]*)mk_test ~n:1000 ~pp:pp_triple ~limit:1 ~name:("find_exn-add_local extensive in " ^ PL.name)

000707| ~size:(fun t -> (*[0]*)String.length (pp_triple t))

000708| Arbitrary.(triple string VL.arb_elem PL.arb_elem)

000709| (fun (s,v,p) -> (*[1000]*)PL.leq p PL.bot (* does not hold for bottom p and non-bottom s,v *)

000710| || (*[920]*)VLAbsPair.leq (v,Abs.bot) (try (*[920]*)PL.find_exn s (PL.add_local s v p)

000711| with Not_found -> (*[0]*)VLAbsPair.bot))

000712|

000713| let find_exn_add_local_monotone = (* forall s,v,v',p. v <= v'

000714| ==> find_exn s (add s v p) <= find_exn s (add s v' p) *)

000715| (*[1]*)let my_pl_find_exn s t = (*[2000]*)try (*[2000]*)PL.find_exn s t

000716| with Not_found -> (*[222]*)VLAbsPair.bot in

000717| (*[1]*)let pp_triple = PP.triple PP.string GenValTests.pp_pair PL.to_string in

000718| (*[1]*)mk_test ~n:1000 ~pp:pp_triple ~limit:1 ~name:("find_exn-add_local monotone in " ^ PL.name)

000719| ~size:(fun t -> (*[0]*)String.length (pp_triple t))

000720| Arbitrary.(triple string GenValTests.ord_pair PL.arb_elem)

000721| (fun (s,(v,v'),p) -> (*[1000]*)Prop.assume (VL.leq v v');

000722| (*[1000]*)VLAbsPair.leq (my_pl_find_exn s (PL.add_local s v p)) (my_pl_find_exn s (PL.add_local s v' p)))

000723|

000724| (* test suite for specific property operations *)

000725| let spec_prop_operations =

000726| (*[1]*)flatten [

000727| is_bot_tests;

000728| find_exn_tests;

000729| find_tests;

000730| find_nonstr_defaults_tests;

000731| find_all_keys_tests;

000732| find_all_tests;

000733| get_metatable_tests;

000734| set_metatable_tests;

000735| [get_metatable_set_metatable_extensive];

000736| set_metatable_absent_tests;

000737| add_tests;

000738| add_local_tests;

000739| add_nonstr_default_tests;

000740| add_scopechain_tests;

000741| add_all_str_tests;

000742| add_all_params_tests;

000743| [ find_add_extensive; find_add_monotone;

000744| find_exn_add_local_extensive; find_exn_add_local_monotone; ] ]

000745|

000746|

000747| (** Store lattice *)

000748|

000749| (* Note: the following predicate depends on the Boolean lattice *)

000750| (* {true,false} under reverse implication ordering. *)

000751| let is_bot_tests =

000752| (*[1]*)let st_is_bot = ("ST.is_bot",ST.is_bot) in

000753| [ (*[1]*)testsig (module ST) -$-> (module Bool) =: st_is_bot;

000754| testsig (module ST) -<-> (module Bool) =: st_is_bot;

000755| testsig (module ST) -~-> (module Bool) =: st_is_bot; ]

000756|

000757| let add_label_tests = (* add_label : ST -> label -> PL -> ST *)

000758| (*[1]*)let st_add_label = ("ST.add_label",ST.add_label) in (* adding entry to bot, or empty table should not give bot *)

000759| [ (*pw_right (module Label) (pw_right (module PL) op_strict) (module ST) (module ST) =:: st_add_label;*)

000760| (*[1]*)pw_right (module Label) (pw_right (module PL) op_monotone) (module ST) (module ST) =:: st_add_label;

000761| pw_right (module Label) (pw_right (module PL) op_invariant) (module ST) (module ST) =:: st_add_label;

000762| (*pw_left (module ST) (pw_left (module Label) op_strict) (module PL) (module ST) =:: st_add_label;*)

000763| pw_left (module ST) (pw_left (module Label) op_monotone) (module PL) (module ST) =:: st_add_label;

000764| pw_left (module ST) (pw_left (module Label) op_invariant) (module PL) (module ST) =:: st_add_label; ]

000765|

000766| let find_label_tests = (* find_label : ST -> label -> PL *)

000767| (*[1]*)let st_find_label = ("ST.find_label",ST.find_label) in

000768| [ (*[1]*)pw_right (module Label) op_strict (module ST) (module PL) =:: st_find_label;

000769| pw_right (module Label) op_monotone (module ST) (module PL) =:: st_find_label;

000770| pw_right (module Label) op_invariant (module ST) (module PL) =:: st_find_label; ]

000771|

000772| let find_label_add_label_id = (* forall s,l,p. find_label (add_label s l p) l = p *)

000773| (*[1]*)let pp_triple = PP.triple ST.to_string PP.int PL.to_string in

000774| (*[1]*)mk_test ~n:1000 ~pp:pp_triple ~limit:1 ~name:("find_label-add_label identity in " ^ ST.name)

000775| ~size:(fun t -> (*[0]*)String.length (pp_triple t))

000776| Arbitrary.(triple ST.arb_elem Label.arb_elem PL.arb_elem)

000777| (fun (s,l,p) -> (*[1000]*)PL.eq (ST.find_label (ST.add_label s l p) l) p)

000778|

000779| let lookup_str_prop_tests = (* lookup_str_prop : ST -> VL -> string -> VL *)

000780| (*[1]*)let st_lookup_str_prop = ("ST.lookup_str_prop",ST.lookup_str_prop) in

000781| [ (*[1]*)pw_right (module VL) (pw_right (module Str_arg) op_strict) (module ST) (module VL) =:: st_lookup_str_prop;

000782| pw_right (module VL) (pw_right (module Str_arg) op_monotone) (module ST) (module VL) =:: st_lookup_str_prop;

000783| pw_right (module VL) (pw_right (module Str_arg) op_invariant) (module ST) (module VL) =:: st_lookup_str_prop;

000784| pw_left (module ST) (pw_right (module Str_arg) op_strict) (module VL) (module VL) =:: st_lookup_str_prop;

000785| pw_left (module ST) (pw_right (module Str_arg) op_monotone) (module VL) (module VL) =:: st_lookup_str_prop;

000786| pw_left (module ST) (pw_right (module Str_arg) op_invariant) (module VL) (module VL) =:: st_lookup_str_prop; ]

000787|

000788| let lookup_all_keys_tests =

000789| (*[1]*)let st_lookup_all_keys = ("ST.lookup_all_keys",ST.lookup_all_keys) in

000790| [ (*[1]*)testsig (module ST) -$-> (module VL) ---> (module VL) =: st_lookup_all_keys;

000791| testsig (module ST) -<-> (module VL) ---> (module VL) =: st_lookup_all_keys;

000792| testsig (module ST) -~-> (module VL) ---> (module VL) =: st_lookup_all_keys;

000793| testsig (module ST) ---> (module VL) -$-> (module VL) =: st_lookup_all_keys;

000794| testsig (module ST) ---> (module VL) -<-> (module VL) =: st_lookup_all_keys;

000795| testsig (module ST) ---> (module VL) -~-> (module VL) =: st_lookup_all_keys; ]

000796|

000797| let lookup_all_str_props_tests =

000798| (*[1]*)let st_lookup_all_str_props = ("ST.lookup_all_str_props",ST.lookup_all_str_props) in

000799| [ (*[1]*)testsig (module ST) -$-> (module VL) ---> (module VL) =: st_lookup_all_str_props;

000800| testsig (module ST) -<-> (module VL) ---> (module VL) =: st_lookup_all_str_props;

000801| testsig (module ST) -~-> (module VL) ---> (module VL) =: st_lookup_all_str_props;

000802| testsig (module ST) ---> (module VL) -$-> (module VL) =: st_lookup_all_str_props;

000803| testsig (module ST) ---> (module VL) -<-> (module VL) =: st_lookup_all_str_props;

000804| testsig (module ST) ---> (module VL) -~-> (module VL) =: st_lookup_all_str_props; ]

000805|

000806| let lookup_all_nonstr_props_tests =

000807| (*[1]*)let st_lookup_all_nonstr_props = ("ST.lookup_all_nonstr_props",ST.lookup_all_nonstr_props) in

000808| [ (*[1]*)testsig (module ST) -$-> (module VL) ---> (module VL) =: st_lookup_all_nonstr_props;

000809| testsig (module ST) -<-> (module VL) ---> (module VL) =: st_lookup_all_nonstr_props;

000810| testsig (module ST) -~-> (module VL) ---> (module VL) =: st_lookup_all_nonstr_props;

000811| testsig (module ST) ---> (module VL) -$-> (module VL) =: st_lookup_all_nonstr_props;

000812| testsig (module ST) ---> (module VL) -<-> (module VL) =: st_lookup_all_nonstr_props;

000813| testsig (module ST) ---> (module VL) -~-> (module VL) =: st_lookup_all_nonstr_props; ]

000814|

000815| let lookup_all_props_tests =

000816| (*[1]*)let st_lookup_all_props = ("ST.lookup_all_props",ST.lookup_all_props) in

000817| [ (*[1]*)testsig (module ST) -$-> (module VL) ---> (module VL) =: st_lookup_all_props;

000818| testsig (module ST) -<-> (module VL) ---> (module VL) =: st_lookup_all_props;

000819| testsig (module ST) -~-> (module VL) ---> (module VL) =: st_lookup_all_props;

000820| testsig (module ST) ---> (module VL) -$-> (module VL) =: st_lookup_all_props;

000821| testsig (module ST) ---> (module VL) -<-> (module VL) =: st_lookup_all_props;

000822| testsig (module ST) ---> (module VL) -~-> (module VL) =: st_lookup_all_props; ]

000823|

000824| let lookup_nonstr_default_prop_tests =

000825| (*[1]*)let st_lookup_nonstr_default_prop = ("ST.lookup_nonstr_default_prop",ST.lookup_nonstr_default_prop) in

000826| [ (*[1]*)testsig (module ST) -$-> (module VL) ---> (module VL) ---> (module VL) =: st_lookup_nonstr_default_prop;

000827| testsig (module ST) -<-> (module VL) ---> (module VL) ---> (module VL) =: st_lookup_nonstr_default_prop;

000828| testsig (module ST) -~-> (module VL) ---> (module VL) ---> (module VL) =: st_lookup_nonstr_default_prop;

000829| testsig (module ST) ---> (module VL) -$-> (module VL) ---> (module VL) =: st_lookup_nonstr_default_prop;

000830| testsig (module ST) ---> (module VL) -<-> (module VL) ---> (module VL) =: st_lookup_nonstr_default_prop;

000831| testsig (module ST) ---> (module VL) -~-> (module VL) ---> (module VL) =: st_lookup_nonstr_default_prop;

000832| testsig (module ST) ---> (module VL) ---> (module VL) -$-> (module VL) =: st_lookup_nonstr_default_prop;

000833| testsig (module ST) ---> (module VL) ---> (module VL) -<-> (module VL) =: st_lookup_nonstr_default_prop;

000834| testsig (module ST) ---> (module VL) ---> (module VL) -~-> (module VL) =: st_lookup_nonstr_default_prop; ]

000835|

000836| let lookup_dyn_prop_tests =

000837| (*[1]*)let st_lookup_dyn_prop = ("ST.lookup_dyn_prop",ST.lookup_dyn_prop) in

000838| [ (*[1]*)testsig (module ST) -$-> (module VL) ---> (module VL) ---> (module VL) =: st_lookup_dyn_prop;

000839| testsig (module ST) -<-> (module VL) ---> (module VL) ---> (module VL) =: st_lookup_dyn_prop;

000840| testsig (module ST) -~-> (module VL) ---> (module VL) ---> (module VL) =: st_lookup_dyn_prop;

000841| testsig (module ST) ---> (module VL) -$-> (module VL) ---> (module VL) =: st_lookup_dyn_prop;

000842| testsig (module ST) ---> (module VL) -<-> (module VL) ---> (module VL) =: st_lookup_dyn_prop;

000843| testsig (module ST) ---> (module VL) -~-> (module VL) ---> (module VL) =: st_lookup_dyn_prop;

000844| testsig (module ST) ---> (module VL) ---> (module VL) -$-> (module VL) =: st_lookup_dyn_prop;

000845| testsig (module ST) ---> (module VL) ---> (module VL) -<-> (module VL) =: st_lookup_dyn_prop;

000846| testsig (module ST) ---> (module VL) ---> (module VL) -~-> (module VL) =: st_lookup_dyn_prop; ]

000847|

000848| let write_str_prop_tests = (* write_str_prop : ST -> VL -> string -> VL -> ST *)

000849| (*[1]*)let wp = ("ST.write_str_prop",ST.write_str_prop) in (* result of writing to empty table should be non bot *)

000850| [ (*[1]*)pw_right (module VL) (pw_right (module Str_arg) (pw_right (module VL) op_strict)) (module ST) (module ST) =:: wp;

000851| pw_right (module VL) (pw_right (module Str_arg) (pw_right (module VL) op_monotone)) (module ST) (module ST) =:: wp;

000852| pw_right (module VL) (pw_right (module Str_arg) (pw_right (module VL) op_invariant)) (module ST) (module ST) =:: wp;

000853| (* pw_left (module ST) (pw_right (module Str_arg) (pw_right (module VL) op_strict)) (module VL) (module ST) =:: wp;*)

000854| pw_left (module ST) (pw_right (module Str_arg) (pw_right (module VL) op_monotone)) (module VL) (module ST) =:: wp;

000855| pw_left (module ST) (pw_right (module Str_arg) (pw_right (module VL) op_invariant)) (module VL) (module ST) =:: wp;

000856| (* pw_left (module ST) (pw_left (module VL) (pw_left (module Str_arg) op_strict)) (module VL) (module ST) =:: wp;*)

000857| pw_left (module ST) (pw_left (module VL) (pw_left (module Str_arg) op_monotone)) (module VL) (module ST) =:: wp;

000858| pw_left (module ST) (pw_left (module VL) (pw_left (module Str_arg) op_invariant)) (module VL) (module ST) =:: wp; ]

000859| (* Current 'write_str_prop' not strict in 2nd and 4th arg *)

000860|

000861| let write_all_str_props_tests = (* result of writing to no table should be bot *)

000862| (*[1]*)let st_write_all_str_props = ("ST.write_all_str_props",ST.write_all_str_props) in

000863| [(*testsig (module ST) -$-> (module VL) ---> (module VL) ---> (module ST) =: st_write_all_str_props;*)

000864| (*[1]*)testsig (module ST) -<-> (module VL) ---> (module VL) ---> (module ST) =: st_write_all_str_props;

000865| testsig (module ST) -~-> (module VL) ---> (module VL) ---> (module ST) =: st_write_all_str_props;

000866| testsig (module ST) ---> (module VL) -$-> (module VL) ---> (module ST) =: st_write_all_str_props;

000867| testsig (module ST) ---> (module VL) -<-> (module VL) ---> (module ST) =: st_write_all_str_props;

000868| testsig (module ST) ---> (module VL) -~-> (module VL) ---> (module ST) =: st_write_all_str_props;

000869| (*testsig (module ST) ---> (module VL) ---> (module VL) -$-> (module ST) =: st_write_all_str_props;*)

000870| testsig (module ST) ---> (module VL) ---> (module VL) -<-> (module ST) =: st_write_all_str_props;

000871| testsig (module ST) ---> (module VL) ---> (module VL) -~-> (module ST) =: st_write_all_str_props; ]

000872| (* Current 'write_all_str_props' not strict in 1st and 3rd args? *)

000873|

000874| let write_default_nonstr_prop_tests = (* result of writing to empty table should not be bot *)

000875| (*[1]*)let st_write_default_nonstr_prop = ("ST.write_default_nonstr_prop",ST.write_default_nonstr_prop) in

000876| [(*testsig (module ST) -$-> (module VL) ---> (module VL) ---> (module VL) ---> (module ST) =: st_write_default_nonstr_prop;*)

000877| (*[1]*)testsig (module ST) -<-> (module VL) ---> (module VL) ---> (module VL) ---> (module ST) =: st_write_default_nonstr_prop;

000878| testsig (module ST) -~-> (module VL) ---> (module VL) ---> (module VL) ---> (module ST) =: st_write_default_nonstr_prop;

000879| (*testsig (module ST) ---> (module VL) -$-> (module VL) ---> (module VL) ---> (module ST) =: st_write_default_nonstr_prop;*)

000880| testsig (module ST) ---> (module VL) -<-> (module VL) ---> (module VL) ---> (module ST) =: st_write_default_nonstr_prop;

000881| testsig (module ST) ---> (module VL) -~-> (module VL) ---> (module VL) ---> (module ST) =: st_write_default_nonstr_prop;

000882| (*testsig (module ST) ---> (module VL) ---> (module VL) -$-> (module VL) ---> (module ST) =: st_write_default_nonstr_prop;*)

000883| testsig (module ST) ---> (module VL) ---> (module VL) -<-> (module VL) ---> (module ST) =: st_write_default_nonstr_prop;

000884| testsig (module ST) ---> (module VL) ---> (module VL) -~-> (module VL) ---> (module ST) =: st_write_default_nonstr_prop;

000885| (*testsig (module ST) ---> (module VL) ---> (module VL) ---> (module VL) -$-> (module ST) =: st_write_default_nonstr_prop;*)

000886| testsig (module ST) ---> (module VL) ---> (module VL) ---> (module VL) -<-> (module ST) =: st_write_default_nonstr_prop;

000887| testsig (module ST) ---> (module VL) ---> (module VL) ---> (module VL) -~-> (module ST) =: st_write_default_nonstr_prop; ]

000888| (* Current 'write_default_nonstr_prop' not strict in 1st, 3rd and 4th args *)

000889|

000890| let write_dyn_prop_tests = (* result of writing to empty table should not be bot *)

000891| (*[1]*)let st_write_dyn_prop = ("ST.write_dyn_prop",ST.write_dyn_prop) in

000892| [(*testsig (module ST) -$-> (module VL) ---> (module VL) ---> (module VL) ---> (module ST) =: st_write_dyn_prop;*)

000893| (*[1]*)testsig (module ST) -<-> (module VL) ---> (module VL) ---> (module VL) ---> (module ST) =: st_write_dyn_prop;

000894| testsig (module ST) -~-> (module VL) ---> (module VL) ---> (module VL) ---> (module ST) =: st_write_dyn_prop;

000895| (*testsig (module ST) ---> (module VL) -$-> (module VL) ---> (module VL) ---> (module ST) =: st_write_dyn_prop;*)

000896| testsig (module ST) ---> (module VL) -<-> (module VL) ---> (module VL) ---> (module ST) =: st_write_dyn_prop;

000897| testsig (module ST) ---> (module VL) -~-> (module VL) ---> (module VL) ---> (module ST) =: st_write_dyn_prop;

000898| (*testsig (module ST) ---> (module VL) ---> (module VL) -$-> (module VL) ---> (module ST) =: st_write_dyn_prop;*)

000899| testsig (module ST) ---> (module VL) ---> (module VL) -<-> (module VL) ---> (module ST) =: st_write_dyn_prop;

000900| testsig (module ST) ---> (module VL) ---> (module VL) -~-> (module VL) ---> (module ST) =: st_write_dyn_prop;

000901| (*testsig (module ST) ---> (module VL) ---> (module VL) ---> (module VL) -$-> (module ST) =: st_write_dyn_prop;*)

000902| testsig (module ST) ---> (module VL) ---> (module VL) ---> (module VL) -<-> (module ST) =: st_write_dyn_prop;

000903| testsig (module ST) ---> (module VL) ---> (module VL) ---> (module VL) -~-> (module ST) =: st_write_dyn_prop; ]

000904| (* Current 'write_dyn_prop' not strict in 1st, 3rd and 4th args *)

000905|

000906| let get_metatable_tests = (* get_metatable : ST -> VL -> VL *)

000907| (*[1]*)let st_get_metatable = ("ST.get_metatable",ST.get_metatable) in

000908| [ (*[1]*)testsig (module ST) -$-> (module VL) ---> (module VL) =: st_get_metatable;

000909| testsig (module ST) -<-> (module VL) ---> (module VL) =: st_get_metatable;

000910| testsig (module ST) -~-> (module VL) ---> (module VL) =: st_get_metatable;

000911| testsig (module ST) ---> (module VL) -$-> (module VL) =: st_get_metatable;

000912| testsig (module ST) ---> (module VL) -<-> (module VL) =: st_get_metatable;

000913| testsig (module ST) ---> (module VL) -~-> (module VL) =: st_get_metatable; ]

000914|

000915| let set_metatable_tests = (* set_metatable : ST -> VL -> VL -> ST *)

000916| (*[1]*)let st_set_metatable = ("ST.set_metatable",ST.set_metatable) in (* result of writing to table-less heap should be bot *)

000917| [ (*[1]*)testsig (module ST) -$-> (module VL) ---> (module VL) ---> (module ST) =: st_set_metatable;

000918| testsig (module ST) -<-> (module VL) ---> (module VL) ---> (module ST) =: st_set_metatable;

000919| testsig (module ST) -~-> (module VL) ---> (module VL) ---> (module ST) =: st_set_metatable;

000920| (*testsig (module ST) ---> (module VL) -$-> (module VL) ---> (module ST) =: st_set_metatable;*)

000921| testsig (module ST) ---> (module VL) -<-> (module VL) ---> (module ST) =: st_set_metatable;

000922| testsig (module ST) ---> (module VL) -~-> (module VL) ---> (module ST) =: st_set_metatable;

000923| (*testsig (module ST) ---> (module VL) ---> (module VL) -$-> (module ST) =: st_set_metatable;*)

000924| testsig (module ST) ---> (module VL) ---> (module VL) -<-> (module ST) =: st_set_metatable;

000925| testsig (module ST) ---> (module VL) ---> (module VL) -~-> (module ST) =: st_set_metatable; ]

000926| (* Current 'set_metatable' not strict in 2nd and 3rd arg *)

000927|

000928| (* not extensive: for empty store, set_metatable will return the empty store

000929| and get_metatable's output will be incomparable to v' *)

000930| (*let get_metatable_set_metatable_extensive = (* forall v,v',st. v' <= get_metatable (set_metatable st v v') v *)

000931| let pp = PP.triple VL.to_string VL.to_string ST.to_string in

000932| mk_test ~n:1000 ~pp:pp ~limit:1 ~size:(fun a -> String.length (pp a))

000933| ~name:("ST.get_meta_table-ST.set_meta_table extensive")

000934| Arbitrary.(triple VL.arb_elem VL.arb_elem ST.arb_elem)

000935| (fun (v,v',st) -> VL.leq (VL.only_tables v') (ST.get_metatable (ST.set_metatable st v (VL.only_tables v')) v)) *)

000936|

000937| let myget_metatable_tests = (* get_metatable : ST -> VL -> VL *)

000938| (*[1]*)let st_myget_metatable = ("ST.myget_metatable",ST.myget_metatable) in

000939| [ (*[1]*)testsig (module ST) -$-> (module VL) ---> (module VL) =: st_myget_metatable;

000940| testsig (module ST) -<-> (module VL) ---> (module VL) =: st_myget_metatable;

000941| testsig (module ST) -~-> (module VL) ---> (module VL) =: st_myget_metatable;

000942| testsig (module ST) ---> (module VL) -$-> (module VL) =: st_myget_metatable;

000943| testsig (module ST) ---> (module VL) -<-> (module VL) =: st_myget_metatable;

000944| testsig (module ST) ---> (module VL) -~-> (module VL) =: st_myget_metatable; ]

000945|

000946| let lookup_event_tests = (* lookup_event : ST -> VL -> string -> VL *)

000947| (*[1]*)let st_lookup_event = ("ST.lookup_event",ST.lookup_event) in

000948| [ (*[1]*)pw_right (module VL) (pw_right (module Str_arg) op_strict) (module ST) (module VL) =:: st_lookup_event;

000949| pw_right (module VL) (pw_right (module Str_arg) op_monotone) (module ST) (module VL) =:: st_lookup_event;

000950| pw_right (module VL) (pw_right (module Str_arg) op_invariant) (module ST) (module VL) =:: st_lookup_event;

000951| pw_left (module ST) (pw_right (module Str_arg) op_strict) (module VL) (module VL) =:: st_lookup_event;

000952| pw_left (module ST) (pw_right (module Str_arg) op_monotone) (module VL) (module VL) =:: st_lookup_event;

000953| pw_left (module ST) (pw_right (module Str_arg) op_invariant) (module VL) (module VL) =:: st_lookup_event; ]

000954|

000955| let getbinhandler_tests = (* getbinhandler : ST -> VL -> VL -> string -> VL *)

000956| (*[1]*)let st_getbinhandler = ("ST.getbinhandler",ST.getbinhandler) in

000957| [ (*[1]*)pw_right (module VL) (pw_right (module VL) (pw_right (module Str_arg) op_strict)) (module ST) (module VL) =:: st_getbinhandler;

000958| pw_right (module VL) (pw_right (module VL) (pw_right (module Str_arg) op_monotone)) (module ST) (module VL) =:: st_getbinhandler;

000959| pw_right (module VL) (pw_right (module VL) (pw_right (module Str_arg) op_invariant)) (module ST) (module VL) =:: st_getbinhandler;

000960| pw_left (module ST) (pw_right (module VL) (pw_right (module Str_arg) op_strict)) (module VL) (module VL) =:: st_getbinhandler;

000961| pw_left (module ST) (pw_right (module VL) (pw_right (module Str_arg) op_monotone)) (module VL) (module VL) =:: st_getbinhandler;

000962| pw_left (module ST) (pw_right (module VL) (pw_right (module Str_arg) op_invariant)) (module VL) (module VL) =:: st_getbinhandler;

000963| pw_left (module ST) (pw_left (module VL) (pw_right (module Str_arg) op_strict)) (module VL) (module VL) =:: st_getbinhandler;

000964| pw_left (module ST) (pw_left (module VL) (pw_right (module Str_arg) op_monotone)) (module VL) (module VL) =:: st_getbinhandler;

000965| pw_left (module ST) (pw_left (module VL) (pw_right (module Str_arg) op_invariant)) (module VL) (module VL) =:: st_getbinhandler; ]

000966|

000967| (* test suite for specific store operations *)

000968| let spec_store_operations =

000969| (*[1]*)flatten [

000970| is_bot_tests;

000971| add_label_tests;

000972| find_label_tests;

000973| [ find_label_add_label_id; ];

000974| lookup_str_prop_tests;

000975| lookup_all_keys_tests;

000976| lookup_all_str_props_tests;

000977| lookup_all_nonstr_props_tests;

000978| lookup_all_props_tests;

000979| lookup_nonstr_default_prop_tests;

000980| lookup_dyn_prop_tests;

000981| write_str_prop_tests;

000982| write_all_str_props_tests;

000983| write_default_nonstr_prop_tests;

000984| write_dyn_prop_tests;

000985| get_metatable_tests;

000986| set_metatable_tests;

000987| (*[get_metatable_set_metatable_extensive];*)

000988| myget_metatable_tests;

000989| lookup_event_tests;

000990| getbinhandler_tests;

000991| ]

000992|

000993|

000994| (** State lattice *)

000995|

000996| (* Note: the following predicate depends on the Boolean lattice *)

000997| (* {true,false} under reverse implication ordering. *)

000998| let is_bot_tests =

000999| (*[1]*)let sl_is_bot = ("SL.is_bot",SL.is_bot) in

001000| [ (*[1]*)testsig (module SL) -$-> (module Bool) =: sl_is_bot;

001001| testsig (module SL) -<-> (module Bool) =: sl_is_bot;

001002| testsig (module SL) -~-> (module Bool) =: sl_is_bot; ]

001003|

001004| (* test suite for specific state operations *)

001005| let app_bi_pair (biname,bi) = ((*[62]*)"SL.apply_builtin " ^ biname, SL.apply_builtin bi)

001006|

001007| let apply_builtin_test_fst p =

001008| (*[29]*)let app_bi_pair = app_bi_pair p in

001009| [ (*[29]*)testsig (module SL) -$-> (module VLlist) ---> (module SLVLlistpair) =: app_bi_pair;

001010| testsig (module SL) -<-> (module VLlist) ---> (module SLVLlistpair) =: app_bi_pair;

001011| testsig (module SL) -~-> (module VLlist) ---> (module SLVLlistpair) =: app_bi_pair; ]

001012|

001013| let apply_builtin_test p =

001014| (*[22]*)let app_bi_pair = app_bi_pair p in

001015| (*[22]*)flatten

001016| [ apply_builtin_test_fst p;

001017| [ testsig (module SL) ---> (module VLlist) -$-> (module SLVLlistpair) =: app_bi_pair;

001018| testsig (module SL) ---> (module VLlist) -<-> (module SLVLlistpair) =: app_bi_pair;

001019| testsig (module SL) ---> (module VLlist) -~-> (module SLVLlistpair) =: app_bi_pair; ]]

001020|

001021| let apply_builtin_tests =

001022| (*[1]*)flatten

001023| [ apply_builtin_test ("VL.Error", VL.Error);

001024| apply_builtin_test ("VL.Exit", VL.Exit);

001025| apply_builtin_test ("VL.Next", VL.Next);

001026| apply_builtin_test ("VL.INext", VL.INext);

001027| apply_builtin_test ("VL.Pairs", VL.Pairs);

001028| apply_builtin_test ("VL.IPairs", VL.IPairs);

001029| apply_builtin_test_fst ("VL.Print", VL.Print); (* note: print not strict in second arg: ok with no args *)

001030| apply_builtin_test_fst ("VL.Write", VL.Write); (* note: write not strict in second arg: ok with no args *)

001031| [ testsig (module SL) ---> (module VLlist) -~-> (module SLVLlistpair) =: (app_bi_pair ("VL.Print",VL.Print));

001032| testsig (module SL) ---> (module VLlist) -<-> (module SLVLlistpair) =: (app_bi_pair ("VL.Print",VL.Print));

001033| testsig (module SL) ---> (module VLlist) -~-> (module SLVLlistpair) =: (app_bi_pair ("VL.Write",VL.Write)); ];

001034| apply_builtin_test ("VL.Tonumber", VL.Tonumber); (* note: write not monotone under above list ordering *)

001035| apply_builtin_test ("VL.Tostring", VL.Tostring);

001036| apply_builtin_test ("VL.Abs", VL.Abs);

001037| apply_builtin_test ("VL.Ceil", VL.Ceil);

001038| apply_builtin_test ("VL.Floor", VL.Floor);

001039| apply_builtin_test ("VL.Mod", VL.Mod);

001040| (*apply_builtin_test ("VL.Random", VL.Random);*)(* random not strict in second arg: ok with no args *)

001041| apply_builtin_test_fst ("VL.Random", VL.Random); (* random not monotone under above list ordering (exactly 0,1,2 args) *)

001042| [testsig (module SL) ---> (module VLlist) -~-> (module SLVLlistpair) =: (app_bi_pair ("VL.Random",VL.Random));];

001043| apply_builtin_test ("VL.Strlen", VL.Strlen);

001044| apply_builtin_test ("VL.Strupper", VL.Strupper);

001045| apply_builtin_test ("VL.Strlower", VL.Strlower);

001046| (*apply_builtin_test ("VL.Strchar", VL.Strchar);*) (* char not strict in second arg: ok with no args *)

001047| apply_builtin_test_fst ("VL.Strchar", VL.Strchar); (* char not monotone under above list ordering *)

001048| [testsig (module SL) ---> (module VLlist) -~-> (module SLVLlistpair) =: (app_bi_pair ("VL.Strchar",VL.Strchar))];

001049| (*apply_builtin_test ("VL.Strbyte", VL.Strbyte);*)

001050| apply_builtin_test_fst ("VL.Strbyte", VL.Strbyte); (* byte not monotone under above list ordering: add non-num args *)

001051| [testsig (module SL) ---> (module VLlist) -$-> (module SLVLlistpair) =: (app_bi_pair ("VL.Strbyte",VL.Strbyte));

001052| testsig (module SL) ---> (module VLlist) -~-> (module SLVLlistpair) =: (app_bi_pair ("VL.Strbyte",VL.Strbyte))];

001053| (*apply_builtin_test ("VL.Strsub", VL.Strsub);*)

001054| apply_builtin_test_fst ("VL.Strsub", VL.Strsub); (* sub not monotone under above list ordering! (exactly 0,1,2 args) *)

001055| [testsig (module SL) ---> (module VLlist) -$-> (module SLVLlistpair) =: (app_bi_pair ("VL.Strsub",VL.Strsub));

001056| testsig (module SL) ---> (module VLlist) -~-> (module SLVLlistpair) =: (app_bi_pair ("VL.Strsub",VL.Strsub));];

001057| apply_builtin_test ("VL.Sqrt", VL.Sqrt);

001058| apply_builtin_test ("VL.Type", VL.Type);

001059| apply_builtin_test ("VL.Format", VL.Format);

001060| (*apply_builtin_test ("VL.Tblconcat", VL.Tblconcat); *)

001061| apply_builtin_test_fst ("VL.Tblconcat", VL.Tblconcat); (* tblconcat not monotone in 2nd arg under above list ordering: add non-num args *)

001062| [testsig (module SL) ---> (module VLlist) -$-> (module SLVLlistpair) =: (app_bi_pair ("VL.Tblconcat",VL.Tblconcat));

001063| testsig (module SL) ---> (module VLlist) -~-> (module SLVLlistpair) =: (app_bi_pair ("VL.Tblconcat",VL.Tblconcat))];

001064| apply_builtin_test ("VL.Getmetatable", VL.Getmetatable);

001065| apply_builtin_test ("VL.Setmetatable", VL.Setmetatable);

001066| apply_builtin_test ("VL.Rawget", VL.Rawget);

001067| apply_builtin_test ("VL.Rawset", VL.Rawset);

001068| ]

001069|

001070| let add_local_tests = (* add_local : SL -> VL -> string -> SL *)

001071| (*[1]*)let sl_add_local = ("SL.add_local",SL.add_local) in

001072| [ (*[1]*)pw_right (module VL) (pw_right (module Str_arg) op_strict) (module SL) (module SL) =:: sl_add_local;

001073| pw_right (module VL) (pw_right (module Str_arg) op_monotone) (module SL) (module SL) =:: sl_add_local;

001074| pw_right (module VL) (pw_right (module Str_arg) op_invariant) (module SL) (module SL) =:: sl_add_local;

001075| pw_left (module SL) (pw_right (module Str_arg) op_strict) (module VL) (module SL) =:: sl_add_local;

001076| pw_left (module SL) (pw_right (module Str_arg) op_monotone) (module VL) (module SL) =:: sl_add_local;

001077| pw_left (module SL) (pw_right (module Str_arg) op_invariant) (module VL) (module SL) =:: sl_add_local; ]

001078|

001079| let add_local_list_tests = (* add_local_list : SL -> VL list -> string list -> SL *)

001080| (*[1]*)let sl_add_local_list = ("SL.add_local_list",SL.add_local_list) in

001081| [ (*[1]*)pw_right (module VLlist) (pw_right (module Strlist) op_strict) (module SL) (module SL) =:: sl_add_local_list;

001082| pw_right (module VLlist) (pw_right (module Strlist) op_monotone) (module SL) (module SL) =:: sl_add_local_list;

001083| pw_right (module VLlist) (pw_right (module Strlist) op_invariant) (module SL) (module SL) =:: sl_add_local_list;

001084| (* pw_left (module SL) (pw_right (module Strlist) op_strict) (module VLlist) (module SL) =:: sl_add_local_list;

001085| pw_left (module SL) (pw_right (module Strlist) op_monotone) (module VLlist) (module SL) =:: sl_add_local_list; *)

001086| pw_left (module SL) (pw_right (module Strlist) op_invariant) (module VLlist) (module SL) =:: sl_add_local_list; ]

001087| (* Current 'add_local_list' not strict in list arg. Not monotone as adding 'no value' will default to nil *)

001088|

001089| let enter_scope_tests = (* enter_scope : SL -> label -> SL *)

001090| (*[1]*)let sl_enter_scope = ("SL.enter_scope",SL.enter_scope) in

001091| [ (*[1]*)pw_right (module Label) op_strict (module SL) (module SL) =:: sl_enter_scope;

001092| pw_right (module Label) op_monotone (module SL) (module SL) =:: sl_enter_scope;

001093| pw_right (module Label) op_invariant (module SL) (module SL) =:: sl_enter_scope; ]

001094|

001095| let build_prop_chain_tests =

001096| (*[1]*)let sl_build_prop_chain = ("SL.build_prop_chain",SL.build_prop_chain) in

001097| [ (*[1]*)testsig (module EL) -$-> (module PL) =: sl_build_prop_chain;

001098| testsig (module EL) -<-> (module PL) =: sl_build_prop_chain;

001099| testsig (module EL) -~-> (module PL) =: sl_build_prop_chain; ]

001100|

001101| let read_name_tests = (* read_name : SL -> string -> VL *)

001102| (*[1]*)let sl_read_name = ("SL.read_name",SL.read_name) in

001103| [ (*[1]*)pw_right (module Str_arg) op_strict (module SL) (module VL) =:: sl_read_name;

001104| pw_right (module Str_arg) op_monotone (module SL) (module VL) =:: sl_read_name;

001105| pw_right (module Str_arg) op_invariant (module SL) (module VL) =:: sl_read_name; ]

001106|

001107| let write_name_tests = (* write_name : SL -> string -> VL -> SL *)

001108| (*[1]*)let sl_write_name = ("SL.write_name",SL.write_name) in

001109| [(*pw_right (module Str_arg) (pw_right (module VL) op_strict) (module SL) (module SL) =:: sl_write_name;*)

001110| (*[1]*)pw_right (module Str_arg) (pw_right (module VL) op_monotone) (module SL) (module SL) =:: sl_write_name;

001111| pw_right (module Str_arg) (pw_right (module VL) op_invariant) (module SL) (module SL) =:: sl_write_name;

001112| (*pw_left (module SL) (pw_left (module Str_arg) op_strict) (module VL) (module SL) =:: sl_write_name;*)

001113| pw_left (module SL) (pw_left (module Str_arg) op_monotone) (module VL) (module SL) =:: sl_write_name;

001114| pw_left (module SL) (pw_left (module Str_arg) op_invariant) (module VL) (module SL) =:: sl_write_name; ]

001115| (* Current 'write_name' not strict in 1st and 3rd args *)

001116|

001117| let write_dyn_prop_tests =

001118| (*[1]*)let sl_write_dyn_prop = ("SL.write_dyn_prop",SL.write_dyn_prop) in

001119| [ (* write_dyn_prop not strict in first arg *)

001120| (*[1]*)testsig (module SL) -<-> (module VL) ---> (module VL) ---> (module VL) ---> (module SL) =: sl_write_dyn_prop;

001121| testsig (module SL) -~-> (module VL) ---> (module VL) ---> (module VL) ---> (module SL) =: sl_write_dyn_prop;

001122| testsig (module SL) ---> (module VL) -<-> (module VL) ---> (module VL) ---> (module SL) =: sl_write_dyn_prop;

001123| testsig (module SL) ---> (module VL) -~-> (module VL) ---> (module VL) ---> (module SL) =: sl_write_dyn_prop;

001124| testsig (module SL) ---> (module VL) ---> (module VL) -<-> (module VL) ---> (module SL) =: sl_write_dyn_prop;

001125| testsig (module SL) ---> (module VL) ---> (module VL) -~-> (module VL) ---> (module SL) =: sl_write_dyn_prop;

001126| testsig (module SL) ---> (module VL) ---> (module VL) ---> (module VL) -<-> (module SL) =: sl_write_dyn_prop;

001127| testsig (module SL) ---> (module VL) ---> (module VL) ---> (module VL) -~-> (module SL) =: sl_write_dyn_prop; ]

001128|

001129| let getbinhandler_tests = (* getbinhandler : SL -> VL -> VL -> string -> VL *)

001130| (*[1]*)let sl_getbinhandler = ("SL.getbinhandler",SL.getbinhandler) in

001131| [ (*[1]*)pw_right (module VL) (pw_right (module VL) (pw_right (module Str_arg) op_strict)) (module SL) (module VL) =:: sl_getbinhandler;

001132| pw_right (module VL) (pw_right (module VL) (pw_right (module Str_arg) op_monotone)) (module SL) (module VL) =:: sl_getbinhandler;

001133| pw_right (module VL) (pw_right (module VL) (pw_right (module Str_arg) op_invariant)) (module SL) (module VL) =:: sl_getbinhandler;

001134| pw_left (module SL) (pw_right (module VL) (pw_right (module Str_arg) op_strict)) (module VL) (module VL) =:: sl_getbinhandler;

001135| pw_left (module SL) (pw_right (module VL) (pw_right (module Str_arg) op_monotone)) (module VL) (module VL) =:: sl_getbinhandler;

001136| pw_left (module SL) (pw_right (module VL) (pw_right (module Str_arg) op_invariant)) (module VL) (module VL) =:: sl_getbinhandler;

001137| pw_left (module SL) (pw_left (module VL) (pw_right (module Str_arg) op_strict)) (module VL) (module VL) =:: sl_getbinhandler;

001138| pw_left (module SL) (pw_left (module VL) (pw_right (module Str_arg) op_monotone)) (module VL) (module VL) =:: sl_getbinhandler;

001139| pw_left (module SL) (pw_left (module VL) (pw_right (module Str_arg) op_invariant)) (module VL) (module VL) =:: sl_getbinhandler; ]

001140|

001141| let spec_state_operations =

001142| (*[1]*)flatten

001143| [ is_bot_tests;

001144| apply_builtin_tests;

001145| add_local_tests;

001146| add_local_list_tests;

001147| enter_scope_tests;

001148| build_prop_chain_tests;

001149| read_name_tests;

001150| write_name_tests;

001151| write_dyn_prop_tests;

001152| getbinhandler_tests; ]

001153|

001154|

001155| (** Analysis lattice *)

001156|

001157| (* test suite for specific analysis operations *)

001158| let lookup_tests = (* lookup : AL -> label -> SL *)

001159| (*[1]*)let al_lookup = ("AL.lookup",AL.lookup) in

001160| [ (*[1]*)pw_right (module Label) op_strict (module AL) (module SL) =:: al_lookup;

001161| pw_right (module Label) op_monotone (module AL) (module SL) =:: al_lookup;

001162| pw_right (module Label) op_invariant (module AL) (module SL) =:: al_lookup; ]

001163|

001164| let add_tests = (* add : AL -> label -> SL -> AL *)

001165| (*[1]*)let al_add = ("AL.add",AL.add) in

001166| [ (* add not strict in either arg *)

001167| (*[1]*)pw_right (module Label) (pw_right (module SL) op_monotone) (module AL) (module AL) =:: al_add;

001168| pw_right (module Label) (pw_right (module SL) op_invariant) (module AL) (module AL) =:: al_add;

001169| pw_left (module AL) (pw_left (module Label) op_monotone) (module SL) (module AL) =:: al_add;

001170| pw_left (module AL) (pw_left (module Label) op_invariant) (module SL) (module AL) =:: al_add; ]

001171|

001172| let spec_analysis_operations =

001173| (*[1]*)flatten [

001174| lookup_tests;

001175| add_tests; ]

001176|

001177|

001178| (** Test suite code *)

001179|

001180| let _ =

001181| (*[1]*)run_tests (*~rand:(Random.State.make_self_init ())*)

001182| (flatten

001183| [(* generic lattice tests *)

001184| GenAbsTests.suite;

001185| GenNumTests.suite;

001186| GenStrTests.suite;

001187| GenValTests.suite;

001188| GenEnvTests.suite;

001189| GenPropTests.suite;

001190| GenStoTests.suite;

001191| GenStaTests.suite;

001192| GenAnaTests.suite;

001193| (* generic lattice top tests *)

001194| GenAbsTopTests.suite;

001195| GenNumTopTests.suite;

001196| GenStrTopTests.suite;

001197| (* tests of helper lattices *)

001198| GenBoolTests.suite;

001199| GenBoolTopTests.suite;

001200| GenDBoolTests.suite;

001201| GenDBoolTopTests.suite;

001202| GenVLAbspairTests.suite;

001203| GenVLVLpairTests.suite;

001204| GenVLlistTests.suite;

001205| GenSLVLlistpairTests.suite;

001206| (* specific lattice operation tests *)

001207| spec_str_operations;

001208| spec_vl_operations;

001209| spec_env_operations;

001210| spec_prop_operations;

001211| spec_store_operations;

001212| spec_state_operations;

001213| spec_analysis_operations; ])