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 =
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') *)
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 *)
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; ])