diff --git a/.gitignore b/.gitignore index 8d39ced..5f0095b 100644 --- a/.gitignore +++ b/.gitignore @@ -32,4 +32,4 @@ yarn-error.log *.swp bin/troupe bin/understudy -trp-rt/out/ +trp-rt/out/ \ No newline at end of file diff --git a/Makefile b/Makefile index 38490f2..422eb12 100644 --- a/Makefile +++ b/Makefile @@ -25,6 +25,7 @@ libs: $(COMPILER) ./lib/raft_debug.trp -l $(COMPILER) ./lib/bst.trp -l $(COMPILER) ./lib/localregistry.trp -l + $(COMPILER) ./lib/troupecheck.trp -l test: mkdir -p out diff --git a/lib/lists.trp b/lib/lists.trp index 482f875..5725846 100644 --- a/lib/lists.trp +++ b/lib/lists.trp @@ -69,5 +69,6 @@ in , ("length", length) , ("append", append) , ("partition", partition) + , ("nth", nth) ] end diff --git a/lib/out/lists.exports b/lib/out/lists.exports index d0a5830..aa028fe 100644 --- a/lib/out/lists.exports +++ b/lib/out/lists.exports @@ -7,4 +7,5 @@ lookup elem length append -partition \ No newline at end of file +partition +nth \ No newline at end of file diff --git a/lib/troupecheck.trp b/lib/troupecheck.trp new file mode 100644 index 0000000..d474d1c --- /dev/null +++ b/lib/troupecheck.trp @@ -0,0 +1,627 @@ +import lists + +(* +-------------------------------- +INIT FUNCTION + +To be called when starting out testing + +-------------------------------- +*) +let fun init_tc auth rng = + receive [hn ("REQUEST_RNG", senderid) => + let val _ = send (senderid, rng) + in init_tc auth rng end, + + hn ("REQUEST_AUTH", senderid) => + let val _ = send (senderid, auth) + in init_tc auth rng end, + + hn ("UPDATE_RNG", senderid, new_rng) => + let val _ = send(senderid, "done") in + init_tc auth new_rng end] + +(* +-------------------------------- +PRINTING TO CONSOLE + +Simple functions for more convenient printing to console. + +-------------------------------- +*) + fun write x auth = + fwrite ((getStdout auth), x) + + fun args_toString args = + let fun aux_toString acc (x0::x1::xs) = aux_toString (acc ^ (toString x0) ^ ", ") (x1::xs) + | aux_toString acc (x::xs) = acc ^ (toString x) in + aux_toString "" args end + +(* +-------------------------------- +ERROR HANDLING + +Handles the printing of appropriate error messages for errors that may occur in the use of TroupeCheck. + +-------------------------------- +*) + fun report_error error_reason tco = + let val _ = send (tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + val err_string = case error_reason of + ("cant_satisfy", tries) => "No valid test could be generated after " ^ (toString tries) ^ " tries.\n" + | ("non_boolean_result", _) => "The property or precondition code returned a non-boolean result.\n" + | ("type_mismatch", _) => "The types' structure doesn't match the property.\n" + | ("record_mismatch", _) => "the number of names provided for record generation, does not match the number of types provided.\n" + in + write "\u001B[31m \nError: " auth; (* Changing the print color to red *) + write (err_string ^ "\u001B[0m") auth; (* Changing the color back *) + exit (auth, 0) end + + fun boolean_check x tco = + if (getType x)<>"boolean" then report_error ("non_boolean_result", 0) tco else () + + fun function_not_done_check p tco = + if (getType p)<>"function" then report_error ("type_mismatch", 0) tco else () +(* +-------------------------------- +UTILS + +Different utility functions that are used across the library. + +-------------------------------- +*) + fun remove_nth n [] i = [] + | remove_nth n (x::xs) i = + if n = i then xs + else x :: (remove_nth n xs (i + 1)) + + fun make_list (f, i) = + case i of + 0 => [] + | _ => append [f()] (make_list (f, i-1)) + + +(* TODO: handle when arguments are passed to a property that does not take arguments *) + fun apply_args p l tco = + let val _ = send (tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + in case l of + [] => (* this case is only reached if there are no generators to begin with *) + let val _ = boolean_check (p()) tco + val res = p() + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + | (x::xs) => + let val res = foldl (fn (x,y) => function_not_done_check y tco; y x) p l + val _ = boolean_check res tco + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + end + + fun report_fail_reason rec noOfTests tco = + let val _ = send (tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] in + case rec.failReason of + "false_prop" => + write "\nFailure at input: " auth; + write (args_toString rec.ctx) auth; + write ("\nAfter running: " ^ (toString (noOfTests - rec.remTests + 1)) ^ " test(s)\n") auth + end + + fun build_record names vals = + let fun aux r [] [] = r + | aux r (n::ns) (v::vs) = + aux (recordExtend(r, n, v)) ns vs in + aux {} names vals + end + + (* Hardcoded until a tuple from list function is implemented in Troupe - an issue has been raised on GH.*) + fun build_tuple ls = + case ls of + [] => (0) + |[x] => (x) + |[x1,x2] => (x1,x2) + |[x1,x2,x3] => (x1,x2,x3) + |[x1,x2,x3,x4] => (x1,x2,x3,x4) + |[x1,x2,x3,x4,x5] => (x1,x2,x3,x4,x5) + |[x1,x2,x3,x4,x5,x6] => (x1,x2,x3,x4,x5,x6) + |[x1,x2,x3,x4,x5,x6,x7] => (x1,x2,x3,x4,x5,x6,x7) + |[x1,x2,x3,x4,x5,x6,x7,x8] => (x1,x2,x3,x4,x5,x6,x7,x8) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9] => (x1,x2,x3,x4,x5,x6,x7,x8,x9) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10] => (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) + |_ => (2, 3, 4, 5) + + fun dec_nth list idx = + let fun dec_nth_aux [] acc i = acc + | dec_nth_aux (x::xs) acc i = + case i = idx of + true => + let val dec_val = if x <= 1/10000 then 0 else x/(3/2) in + append (append acc [dec_val]) xs end + | false => dec_nth_aux xs (append acc [x]) (i+1) + in + dec_nth_aux list [] 0 end + + fun zero_nth list idx = + let fun zero_nth_aux [] acc i = acc + | zero_nth_aux (x::xs) acc i = + case i = idx of + true => + append (append acc [0]) xs + | false => zero_nth_aux xs (append acc [x]) (i+1) + in + zero_nth_aux list [] 0 end + + fun dec_all seq = + let fun dec_all_aux [] i = [] + | dec_all_aux (x::xs) i = + if x = 0 then + dec_all_aux xs (i+1) + else + [(fn () => (zero_nth seq i)), (fn() => [fn () => (dec_nth seq i), fn () => dec_all_aux xs (i+1)])] in + dec_all_aux seq 0 end + + fun seqs_of_seq sequence lengths = + let fun aux seq acc 0 = (acc, seq) + | aux (x::xs) acc n = + aux xs (append acc [x]) (n-1) + val (res, _) = (foldl (fn (x,(acc, s)) => + let val (curr_acc, curr_seq) = aux s [] x in + (append acc [curr_acc], curr_seq) end)([], sequence) lengths) + in res + end + + fun cutoff_at list idx = + let fun aux ls acc 0 = acc + | aux (x::xs) acc i = + aux xs (append acc [x]) (i-1) in + aux list [] idx end + + fun for_i f y 0 = y + | for_i f y i = for_i f (f (i,y)) (i-1) +(* +-------------------------------- +SHRINKING + +Works by first using random shrinking when a failing example has been found (shrink & random_shrink_aux). +Random shrinking means simply generating new test cases with gradually smaller size, to find a case smaller than the original one. This rarely produces a minmal result. +The smallest randomly shrunk instance is then further shrunk using internal shrinking. (internal_shrink & internal_shrink_aux) +Internal shrinking means keeping track of all random decision made during generation, and then re-generating with smaller "random" decisions. + +This part of the code also contains the functionality for recording all random decisions, and replaying these random decisions (rec_rng & rep_rng). +All of these functions are spawned and then requests or updates may be send to them, so that the correct RNG's are used at different points in the code. + +-------------------------------- +*) + fun rec_rng ls = + receive [hn ("REQUEST_RND", senderid) => + let val rnd = random() + val _ = send (senderid, rnd) + in rec_rng (rnd :: ls) + end, + hn ("REQUEST_SEQ", senderid) => + let val _ = send (senderid, (reverse ls)) + in rec_rng [] + end] + + fun rep_rng ls = + receive [hn ("REQUEST_RND", senderid) => + case ls of + (x::xs) => + let val _ = send (senderid, x) + in rep_rng xs + end + | [] => + let val _ = send (senderid, 0) + in rep_rng ls + end, + hn ("REQUEST_LEFT", senderid) => + let val _ = send (senderid, ls) + in rep_rng [] + end, + hn ("UPDATE_LS", new_ls) => + rep_rng new_ls] + + fun shrink_sized_sequence seqs gens prop pre size left_over_len idx_of_sized tco = + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val _ = send(tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + val cap = ceil (((length (nth seqs (idx_of_sized+1)))-2)/left_over_len )(* number of to remove parts of the sequence *) + val size_ls = for_i (fn (x,y) => append y [x]) [] (left_over_len-1) + fun aux i = + let val to_remove = foldl (fn (x,y) => append y [(i*left_over_len)-x])[i*left_over_len] size_ls + val new_seq = foldl (fn (x,y) => remove_nth x y 0) (nth seqs (idx_of_sized+1)) to_remove + val new_seqs = mapi (fn (i, x) => if i = idx_of_sized then new_seq else x) seqs + val new_args = mapi (fn (i, x) => + let val _ = send (pid, ("UPDATE_LS", (nth new_seqs (i+1)))) + val arg = x tco size + in arg + end) gens + in case i = (cap) of + true => + (new_seqs, new_args) + | false => + let val precond_is_met = if (pre <> ()) then (apply_args pre new_args tco) else true + in case (apply_args prop new_args tco) orelse (precond_is_met = false) of + true => aux (i+1) + | false => (new_seqs, new_args) + end + end + in aux 1 + end + + + + fun internal_shrink_aux seqs gens lengths prop pre size counter tco = + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val _ = send(tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + in case seqs of + (x1::x2::x3::xs) => + let val seqs_of_curr = seqs_of_seq (x2()) lengths + val args_and_leftovers = mapi (fn (i, x) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = x tco size + val _ = send (pid, ("REQUEST_LEFT", self())) + val left_overs = receive [hn x => x] + in {arg = arg, left_overs = left_overs} + end) gens + val (test_args, left_over_seqs) = foldl (fn (x, (raws, left_overs)) => (append raws [x.arg], append left_overs [x.left_overs])) ([],[]) args_and_leftovers + (* val ret_seqs = mapi (fn (i,x) => + if (length x) = 0 then (nth seqs_of_curr (i+1)) + else cutoff_at (nth seqs_of_curr (i+1)) ((nth lengths (i+1))-(length x))) left_over_seqs *) + val (is_sized_sequence, idx_of_sized, left_over_size, _) = foldl (fn (x,(bool, idx, len, count)) => if (length x > 0) + then (true, count, (length x), (count+1)) + else (bool, idx, len, (count+1))) (false, -1, 0, 0) left_over_seqs + + val (ret_seqs, args) = if is_sized_sequence + then shrink_sized_sequence seqs_of_curr gens prop pre size left_over_size idx_of_sized tco + else (seqs_of_curr, test_args) + val precond_is_met = if (pre <> ()) then (apply_args pre args tco) else true + in + case (apply_args prop args tco) orelse (precond_is_met = false) of + true => internal_shrink_aux (x1::x3()) gens lengths prop pre size counter tco + | false => internal_shrink ret_seqs gens prop pre size (counter+1) tco + end + | (x::xs) => + let val seqs_of_curr = seqs_of_seq (x()) lengths + val test_args = mapi (fn (i, y) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = y tco size + in arg end) gens + val precond_is_met = if (pre <> ()) then (apply_args pre test_args tco) else true + in + case (apply_args prop test_args tco) orelse (precond_is_met = false) orelse (size < 0) of + true => + let val res = mapi (fn (i, y) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = y tco (size+1) + in arg end) gens in + {shrunk_ctx = res, count = counter} end + | false => internal_shrink_aux [x] gens lengths prop pre (size-1) counter tco + + end + end + + and internal_shrink sequences gens prop pre size counter tco = + let val (seqs_comb, seq_lengths) = foldl (fn (x, (seq, lengths)) => ((append seq x), (append lengths [(length x)]))) ([], []) sequences + in + if foldl (fn (x,y) => (x = 0) andalso y) true seqs_comb then + internal_shrink_aux [fn () => seqs_comb] gens seq_lengths prop pre size counter tco + else + let val decreased_seqs = dec_all seqs_comb + val dec_seqs_w_root = append [fn() => seqs_comb] decreased_seqs + val res = internal_shrink_aux dec_seqs_w_root gens seq_lengths prop pre size (counter) tco + in + res end + end + + fun random_shrink_aux sequences generators prop pre success size counter divi tco = + if (counter = 100) orelse (size = 0) then {count = success, size = size, sequences = sequences} else + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val new_size = floor (size/divi) + val (shrunk_args, shrunk_sequences) = + foldl (fn (x, (arg_acc, seq_acc)) => + let val arg = x tco new_size + val _ = send (pid, ("REQUEST_SEQ", self())) + val seq = receive [hn x => x] + in (append arg_acc [arg], append seq_acc [seq]) + end) ([],[]) generators + val precond_is_met = if (pre <> ()) then (apply_args pre shrunk_args tco) else true + in + case (apply_args prop shrunk_args tco) orelse (precond_is_met = false) of + true => random_shrink_aux sequences generators prop pre success size (counter+1) (divi+2) tco + | false => + random_shrink_aux shrunk_sequences generators prop pre (success+1) new_size (0) 2 tco + end + + fun shrink sequence generators prop pre size counter tco = + let val rng_recorder = spawn (fn() => rec_rng []) + val _ = send (tco, ("UPDATE_RNG", self(), rng_recorder)) + val _ = receive [hn x => ()] + val res = random_shrink_aux sequence generators prop pre 0 size counter 2 tco + val rng_replayer = spawn (fn() => rep_rng []) + val _ = send (tco, ("UPDATE_RNG", self(), rng_replayer)) + val _ = receive [hn x => ()] + val res = internal_shrink (res.sequences) generators prop pre res.size (res.count) tco + in + res + end +(* +-------------------------------- +GENERATORS + +Contains generators for Troupe's built-in types. All generators must return a single instance of the type they generate, +and take a 'size' argument as the very last argument. +This size will be given to all generators in the generation of test cases (and shrinking). +Generators that take more arguments, will need to have these passed along to them before passing the generator to the testing facilities +(convenience functions for this are supplied later). + +It is recommended that all user defined generators only make use of pre-defined generators or their matching convenience functions +for random decisions (i.e. a call to float_gen/float() or int_gen/integer()), instead of having to send and receive the correct messages to the RNG threads. +However, it can be done if the users wishes to and understands what is going on. + +-------------------------------- +*) + + fun float_gen (low, high) tco size = + let val _ = send (tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + + val _ = send (pid, ("REQUEST_RND", self())) + val x = receive [hn x => x] + + val _ = send (pid, ("REQUEST_RND", self())) + val bool_int = receive [hn x => x] + + val bool = bool_int < (1/2) + + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + + val res = + case (lInf, hInf) of + (true, true) => if bool then x * size else -x * size + | (true, false) => high - (x * size) + | (false, true) => low + (x * size) + | (false, false) => low + (x * (high-low)) + in res + end + + fun int_gen (low, high) tco size = + let val res = floor (float_gen (low, high+1) tco size) + in res + end + + fun one_of ls tco size = + let val idx = (int_gen (1, (length ls)) tco size) + in (nth ls idx) + end + + fun bool_gen tco size = + let val rnd = int_gen (0,1) tco size + val res = if rnd = 0 then false + else true + in res + end + + (* NOTE: Generates only letters (upper and lower case) and numbers. *) + fun char_gen tco size = + let val chars = + ["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", + "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", + "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", + "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", + "0", "1", "2", "3", "4", "5", "6", "7", "8", "9"] (* length: 62 *) + val x = (int_gen (1, (62-1)) tco size) + in nth chars x + end + + fun label_gen tco size = + newlabel() + + (* ts: list of generators - used to generate values for fields *) + (* NOTE: Hardcoded for tuple of up to 10 elements - see build_tuple in 'UTILS' *) + fun tuple_gen ts tco size = + let val ts_vals = map (fn x => x tco size) ts + in build_tuple ts_vals + end + + (* ns: list of strings - will be used as fieldnames *) + (* ts: list of generators - used to generate values for fields *) + fun rec_gen ns ts tco size = + if (length ns) <> (length ts) then + report_error ("record_mismatch", 0) tco + else + let val ts_vals = map (fn x => x tco size) ts + val res = build_record ns ts_vals + in res + end + + fun labeled_value_gen labels value_gen tco size = + let val inst = value_gen tco size + val lab = one_of labels tco size + in inst raisedTo lab + end + + fun combined_labeled_gen labels gen tco size = + let val labels_to_use = foldl(fn (x,y) => if (bool_gen tco size) then append y [x] else y)[`{}`] labels + val value = gen tco size + val res = foldl (fn (x,y) => y raisedTo x) value labels_to_use + in res + end + + (* NOTE: Generates only strings of letters (upper and lower case) and numbers. *) + fun string_gen tco size = + let val len = (int_gen (0, size) tco size) + fun string_aux acc 0 = acc + | string_aux acc i = string_aux ((char_gen tco size) ^ acc) (i-1) + val string = (string_aux "" len) + in string + end + + fun list_gen (generator) tco size = + let val len = (int_gen (0, size) tco size) + val res = make_list ((fn () => generator tco size), len) + in res + end + +(* +-------------------------------- +CORE FUNCTIONALITY + +Handles preparing the recorder RNG, running the tests, calling the shrinker, and reporting the results to the user. + +-------------------------------- +*) + fun core_forall (generators, prop, 0, size, pre, cap, tco) = {failReason = (), ctx = (), ctx_seq = (), remTests = 0, size = size} + |core_forall (generators, prop, i, size, pre, cap, tco) = + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val _ = send(tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + val (args, sequences) = foldl (fn (x, (arg_acc, seq_acc)) => + let val arg = x tco size + val _ = send (pid, ("REQUEST_SEQ", self())) + val seq = receive [hn x => x] + in (append arg_acc [arg], append seq_acc [seq]) + end) ([],[])generators + in + case pre of + () => + if (apply_args prop args tco) then + let val _ = write "." auth + in core_forall (generators, prop, i-1, size+1, pre, cap, tco) + end + else + let val _ = write "!" auth + in {failReason = "false_prop", ctx = args, ctx_seq = sequences, remTests = i, size = size} + end + | _ => + if (apply_args pre args tco) then + if (apply_args prop args tco) then (write "." auth; core_forall (generators, prop, i-1, size+1, pre, cap, tco)) + else + let val _ = write "!" auth + in {failReason = "false_prop", ctx = args, ctx_seq = sequences, remTests = i, size = size} + end + else + let val _ = write "x" auth + in if (size = cap) andalso (i*5 = cap) then report_error ("cant_satisfy", size) tco + else if size = cap then {failReason = (), ctx = (), ctx_seq = (), remTests = i, size = size} + else core_forall (generators, prop, i, size+1, pre, cap, tco) + end + end + + fun run_tests (generators, p, to_shrink, noOfTests) auth = + let val (prop, pre) = + case p of + (x,y) => (x,y) + | x => (x, ()) + val rng_recorder = spawn (fn() => rec_rng []) + val tco = spawn (fn() => init_tc auth rng_recorder) + val res = core_forall (generators, prop, noOfTests, 0, pre, (noOfTests*5), tco) in + case res.failReason of + () => write ("\u001B[1m \u001B[32m \nSuccess: \u001B[0mPassed all " ^ (toString noOfTests) ^ " test(s).\n") auth; true + |_ => + report_fail_reason res noOfTests tco; + if to_shrink then + (write ("\u001B[1m\u001B[34mShrinking\u001B[0m:") auth; + let val shrink_res = shrink res.ctx_seq generators prop pre res.size 0 tco in + write "\nFailing test case was shrunk to:\n" auth; + write (args_toString shrink_res.shrunk_ctx) auth; + write ("\nAfter " ^ (toString shrink_res.count) ^ " iterations.\n") auth; + false + end) + else + false + end + + fun for_all (generators, p) auth = run_tests (generators, p, true, 100) auth + | for_all (generators, p, noOfTests) auth = run_tests (generators, p, true, noOfTests) auth + + fun for_all_noshrink (generators, p) auth = run_tests (generators, p, false, 100) auth + | for_all_noshrink (generators, p, noOfTests) auth = run_tests (generators, p, false, noOfTests) auth + + fun troupecheck props auth = + let val n = toString (length props) + fun troupecheck_aux [] i = exit(auth, 0) + | troupecheck_aux (x::xs) i = + let val _ = write ("\nRunning test " ^ (toString i) ^ " of " ^ n ^ ":\n") auth + val res = x() auth + in troupecheck_aux xs (i+1) end + in troupecheck_aux props 1 + end + +(* +-------------------------------- +CONVENIENCE FUNCTIONS + +These are functions that make it easier for the user to make use of the different generators, and define their own generators. + +-------------------------------- +*) + val inf = 1 / 0 + fun integer () = int_gen(inf, inf) + | integer (l, h) = int_gen(l, h) + + fun pos_integer () = integer(0, inf) + + fun neg_integer () = integer(inf, -1) + + fun float () = float_gen(inf, inf) + | float (h, l) = float_gen(h, l) + + fun pos_float () = float(0, inf) + + fun neg_float () = float(inf, 0) + + fun boolean () = bool_gen + + fun list (type) = list_gen (type) + + fun string () = string_gen + + fun char () = char_gen + + + fun tuple (ts) = tuple_gen ts + + fun labeled_value (ls, gen) = labeled_value_gen ls gen + + fun combined_labeled_value (ls, gen) = combined_labeled_gen ls gen + + fun label() = label_gen + + fun record (ns, ts) = rec_gen ns ts +in + [ ("make_list", make_list) + , ("build_record", build_record) + , ("build_tuple", build_tuple) + , ("one_of", one_of) + , ("for_all", for_all) + , ("for_all_noshrink", for_all_noshrink) + , ("troupecheck", troupecheck) + , ("inf", inf) + , ("integer", integer) + , ("pos_integer", pos_integer) + , ("neg_integer", neg_integer) + , ("float", float) + , ("pos_float", pos_float) + , ("neg_float", neg_float) + , ("boolean", boolean) + , ("list", list) + , ("string", string) + , ("char", char) + , ("tuple", tuple) + , ("labeled_value", labeled_value) + , ("combined_labeled_value", combined_labeled_value) + , ("label", label) + , ("record", record) + ] +end diff --git a/tests/rt/pos/core/nth1.golden b/tests/rt/pos/core/nth1.golden new file mode 100644 index 0000000..20ad979 --- /dev/null +++ b/tests/rt/pos/core/nth1.golden @@ -0,0 +1,2 @@ +2024-06-09T16:24:36.820Z [RTM] info: Skipping network creation. Observe that all external IO operations will yield a runtime error. +>>> Main thread finished with value: 2@{}%{} diff --git a/tests/rt/pos/core/nth1.trp b/tests/rt/pos/core/nth1.trp new file mode 100644 index 0000000..fe5b7fc --- /dev/null +++ b/tests/rt/pos/core/nth1.trp @@ -0,0 +1,4 @@ +import lists +let val ls = [1,2,3,4] +in nth ls 2 +end \ No newline at end of file diff --git a/tests/rt/pos/core/nth2.golden b/tests/rt/pos/core/nth2.golden new file mode 100644 index 0000000..76123f6 --- /dev/null +++ b/tests/rt/pos/core/nth2.golden @@ -0,0 +1,2 @@ +2024-06-09T16:28:52.670Z [RTM] info: Skipping network creation. Observe that all external IO operations will yield a runtime error. +>>> Main thread finished with value: true@{}%{} diff --git a/tests/rt/pos/core/nth2.trp b/tests/rt/pos/core/nth2.trp new file mode 100644 index 0000000..e832b84 --- /dev/null +++ b/tests/rt/pos/core/nth2.trp @@ -0,0 +1,8 @@ +import lists +let val ls = ["ls", 3, 1/2, {r = 10, p = 7}] + val string = nth ls 1 + val int = nth ls 2 + val float = nth ls 3 + val record = nth ls 4 +in (getType string = "string") andalso (getType int = "number") andalso (getType float = "number") andalso (getType record = "record") +end diff --git a/troupecheck/Makefile b/troupecheck/Makefile new file mode 100644 index 0000000..b38299f --- /dev/null +++ b/troupecheck/Makefile @@ -0,0 +1,8 @@ +TLOCAL=$(TROUPE)/local.sh + +tc-tests: + $(TLOCAL) ./tc_tests/general-testing.trp + $(TLOCAL) ./tc_tests/userguide-tests.trp + +tc-shrink-tests: + $(TLOCAL) ./tc_tests/shrinking-tests.trp \ No newline at end of file diff --git a/troupecheck/battleship/Makefile b/troupecheck/battleship/Makefile new file mode 100644 index 0000000..94b34ed --- /dev/null +++ b/troupecheck/battleship/Makefile @@ -0,0 +1,20 @@ +MKID=node $(TROUPE)/rt/built/p2p/mkid.mjs +MKALIASES=node $(TROUPE)/rt/built/p2p/mkaliases.js +START=$(TROUPE)/network.sh + +battleship-game: + + $(START) battleship-game.trp --id=ids/battleship-game.json --port=6789 # --debug --debugp2p + +battleship-player1: + $(START) battleship-player.trp --id=ids/battleship-player1.json --aliases=aliases.json # --debug --debugp2p + +battleship-player2: + $(START) battleship-player.trp --id=ids/battleship-player2.json --aliases=aliases.json # --debug --debugp2p + +create-network-identifiers: + mkdir -p ids + $(MKID) --outfile=ids/battleship-game.json + $(MKID) --outfile=ids/battleship-player1.json + $(MKID) --outfile=ids/battleship-player2.json + $(MKALIASES) --include ids/battleship-game.json --include ids/battleship-player1.json --include ids/battleship-player2.json --outfile aliases.json diff --git a/troupecheck/battleship/README.md b/troupecheck/battleship/README.md new file mode 100644 index 0000000..54dbc51 --- /dev/null +++ b/troupecheck/battleship/README.md @@ -0,0 +1,8 @@ +# Battleship game example + +1. *First-time only* Run `make create-network-identifiers`. This command will create two network identifiers in the local subdirectory `ids/`, and an alias file with the generated identifiers. + +2. Run the server by running `make battleship-game` +3. Open another terminal window and start player 1 by running `make battleship-player1` +4. Open another terminal window again and start player 2 by running `make battleship-player2` + diff --git a/troupecheck/battleship/aliases.json b/troupecheck/battleship/aliases.json new file mode 100644 index 0000000..1e90cdc --- /dev/null +++ b/troupecheck/battleship/aliases.json @@ -0,0 +1 @@ +{"battleship-game":"12D3KooWLz6JNygFFtyTjujjU29ivACgp9bxYGCHheoyfwxpgpv7","battleship-player1":"12D3KooWCCB5cy5eYhdrzPqUqYbmcQjKiKjBA8EH3jvtP5R6jkxc","battleship-player2":"12D3KooWQwT7Pv3vVTZjkhztwU4zzp3mNMQSstzkN2vvNai4uqNv"} \ No newline at end of file diff --git a/troupecheck/battleship/battleship-game.trp b/troupecheck/battleship/battleship-game.trp new file mode 100644 index 0000000..75360d6 --- /dev/null +++ b/troupecheck/battleship/battleship-game.trp @@ -0,0 +1,336 @@ +import lists +import timeout +import troupecheck +let fun make_row (f, i) = + case i of + 0 => [] + | _ => append (make_row (f, i-1)) [f i] + + fun update_board board (x,y) marker = + let val y_ls = nth board y + val new_y = make_row ((fn i => if (i = x) then marker else (nth y_ls i)), 10) + val new_board = make_row ((fn i => if i = y then new_y else (nth board i)), 10) + in new_board + end + + fun check_attack board (x,y) = + if (x > 10) orelse (y > 10) orelse (x < 1) orelse (y < 1) then "Illegal coordinate" + else + let val coord = nth (nth board y) x + in case coord of + "-" => "Miss" + |"O" => "Illegal coordinate" + |"X" => "Illegal coordinate" + |_ => "Hit" + end + + fun update_ship ship (x,y) = + let val res = foldl (fn (z,w) => if z = (x,y) then w else append w [z]) [] ship + in res + end + + + fun update_ships ships (x,y) = + let val interim_ships = map (fn z => update_ship z (x,y)) ships + val res = foldl (fn (z,w) => if (length z) = 0 then w else (append w [z])) [] interim_ships + in res + end + + + fun do_attack board ships (x,y) = + case check_attack board (x,y) of + "Illegal coordinate" => ("Illegal coordinate", board, ships) + | "Miss" => + let val updated_board = (update_board board (x,y) "O") + in ("Miss", updated_board, ships) + end + | "Hit" => + let val updated_board = (update_board board (x,y) "X") + val updated_ships = (update_ships ships (x,y)) + in ("Hit", updated_board, updated_ships) + end + + fun switch_turn turn = + if turn = 1 then 2 else 1 + + fun declassify_board board = + let val _ = blockdecl authority + val board_decl = (declassify(board, authority, `{}`)) + val res = map (fn x => + let val x_decl = (declassify(x, authority, `{}`)) + in map (fn y => + declassify(y, authority, `{}`)) x_decl + end) board_decl + in res + end + + + fun game p1 p2 turn = + let val player_in = if turn = 1 then p1 else p2 + val player_out = if turn = 1 then p2 else p1 + val _ = send(player_in.id, ("YOURTURN", self())) + in + receive [hn (("ATTACK", x), senderid) => + let val (msg, new_board, new_ships) = do_attack player_out.board player_out.ships x + val _ = blockdecl authority + val msg_decl = declassify (msg, authority, `{}`) + val ships_decl = declassify (new_ships, authority, `{}`) + val board_decl = declassify_board new_board (* (new_board, authority, `{}`) *) + val next_turn = if msg_decl = "Illegal coordinate" then turn else switch_turn turn + in if length ships_decl = 0 then + let val _ = send (senderid, "YOUWON") + val _ = send (player_out.id, ("YOULOST", board_decl, x)) + in exitAfterTimeout authority 10 0 "Game has ended." + end + else + let val _ = send (senderid, (("ATTACK_RESP", msg_decl), self())) + val _ = send (player_out.id, ("UPDATE_MSG", x, msg_decl, board_decl)) + in if turn = 2 + then game {p1 with board = new_board, ships = new_ships} p2 next_turn + else game p1 {p2 with board = new_board, ships = new_ships} next_turn + end + end + ] + end + + val _ = register ("battleship", self(), authority) + + fun setup p1 count = + receive [hn ("JOINING", board, ships, senderid) => + case count of + 1 => + let val p2 = {board = (board raisedTo `{p2}`), id = senderid, ships = (ships raisedTo `{p2}`)} + val _ = send (p1.id, ("STARTING", 1)) + val _ = send (p2.id, ("STARTING", 2)) + in game p1 p2 1 + end + |0 => + setup {board = (board raisedTo `{p1}`), id = senderid, ships = (ships raisedTo `{p1}`)} (count+1)] + +(* +---------------------------- +Testing the game host using TroupeCheck +---------------------------- +*) + fun for_i body acc 0 = acc.0 + | for_i body acc to = for_i body (body acc) (to-1) + + fun bound_from_ship ship = + case ship of + "C" => 5 + | "B" => 4 + | "S" => 3 + | "D" => 2 + + fun update_board_creation board_or_error coordinate = + case getType board_or_error of + "string" => board_or_error + | _ => + let fun place_horizontal (x, y) ship_type board = + let val y_ls = nth board y + val upperbound = x + (bound_from_ship ship_type) + val is_valid = (x >= 1) andalso (upperbound <= 11) + in if is_valid then + let val new_y = make_row ((fn i => if (i >= x) andalso (i < upperbound) then ship_type else (nth y_ls i)), 10) + val new_board = make_row ((fn i => if i = y then new_y else (nth board i)), 10) + in new_board + end + else + ("Invalid coordinates for ship of type: " ^ ship_type) + end + + fun place_vertical (x, y) ship_type board = + let val upperbound = y + (bound_from_ship ship_type) + val is_valid = (x >= 1) andalso (upperbound <= 11) + in if is_valid then + let val new_board = make_row ((fn i => + if i >= y andalso i < upperbound then + make_row ((fn j => if j = x then ship_type else nth (nth board i) j), 10) + else nth board i), 10) + in new_board + end + else + ("Invalid coordinates for ship of type: " ^ ship_type) + end + val ((x,y), direction, ship) = coordinate + in case direction of + "v" => place_vertical (x,y) ship board_or_error + | "h" => place_horizontal (x,y) ship board_or_error + end + + fun ship_coords_from_info info = + let val (org_x, org_y) = info.0 + val count = (bound_from_ship info.2)-1 + in case info.1 of + "h" => + let val coords = for_i (fn acc => (append acc.0 [((acc.1)+1, org_y)], (acc.1)+1)) ([info.0], org_x) count + in coords + end + |"v" => + let val coords = for_i (fn acc => (append acc.0 [(org_x, (acc.1)+1)], (acc.1)+1)) ([info.0], org_y) count + in coords + end + end + + fun make_board ls = + let val start_board = make_row ((fn _ => make_row ((fn _ => "-"), 10)), 10) + val (board, ships) = foldl (fn (x,(board_acc, ships_acc)) => (update_board_creation board_acc x, append ships_acc [ship_coords_from_info x])) (start_board, []) ls + in + (board, ships) + end + + fun remove_elem elem [] = [] + | remove_elem elem (x::xs) = + if elem = x then + xs + else + x :: (remove_elem elem xs) + + + fun remove_available_coords available_coords coords (x,y) dir length = + let val to_remove = + case dir of + "h" => + let val to_remove_interim = for_i (fn (ls, count) => (append ls [(count, y)], (count-1))) (coords, (x-1)) (length-1) + in foldl (fn (c, acc) => + let val interim_x = c.0 + val interim_y = c.1 + val new_ls = + for_i (fn (ls, count) => + (append ls [(interim_x, (interim_y-count))], (count+1))) ([], 1) (length-1) + in append acc new_ls end) to_remove_interim coords + end + + | "v" => + let val to_remove_interim = for_i (fn (ls, count) => (append ls [(x, count)], (count-1))) (coords, (y-1)) (length-1) + in foldl (fn (c, acc) => + let val interim_x = c.0 + val interim_y = c.1 + val new_ls = + for_i (fn (ls, count) => + (append ls [((interim_x-count), interim_y)], (count+1))) ([], 1) (length-1) + in append acc new_ls end) to_remove_interim coords + end + val new_available = foldl (fn (x, y) => remove_elem x y) available_coords to_remove + in + new_available + end + + fun ship_gen available_coords ship_type tco size = + let val dir = one_of ["h", "v"] tco size + val (coord, coords) = case dir of + "h" => + let val avail = + case ship_type of + "C" => + available_coords.c_h + | "B" => + available_coords.b_h + | "S" => + available_coords.s_h + | "D" => + available_coords.d_h + val coord = one_of avail tco size + val coords = ship_coords_from_info (coord, "h", ship_type) + in (coord, coords) + end + | "v" => + let val avail = + case ship_type of + "C" => + available_coords.c_v + | "B" => + available_coords.b_v + | "S" => + available_coords.s_v + | "D" => + available_coords.d_v + val coord = one_of avail tco size + val coords = ship_coords_from_info (coord, "v", ship_type) + in (coord, coords) + end + + val newC_h = remove_available_coords available_coords.c_h coords coord dir 5 + val newC_v = remove_available_coords available_coords.c_v coords coord dir 5 + val newB_h = remove_available_coords available_coords.c_h coords coord dir 4 + val newB_v = remove_available_coords available_coords.c_v coords coord dir 4 + val newS_h = remove_available_coords available_coords.c_h coords coord dir 3 + val newS_v = remove_available_coords available_coords.c_v coords coord dir 3 + val newD_h = remove_available_coords available_coords.c_h coords coord dir 2 + val newD_v = remove_available_coords available_coords.c_v coords coord dir 2 + in ((coord, dir, ship_type), {c_h = newC_h, c_v = newC_v, b_h = newB_h, b_v = newB_v, d_h = newS_h, s_h = newS_h, s_v = newS_v, d_h = newD_h, d_v = newD_v}) + end + + fun make_init_avail_rec () = + let fun remove_elem_xs elem [] = [] + | remove_elem_xs elem (x::xs) = + if (elem = (x.0)) then + remove_elem_xs elem xs + else + x :: (remove_elem_xs elem xs) + + fun remove_elem_ys elem [] = [] + | remove_elem_ys elem (x::xs) = + if (elem = (x.1)) then + remove_elem_ys elem xs + else + x :: (remove_elem_ys elem xs) + + val init = for_i (fn (acc, x_count) => + let val list = for_i (fn (acc, y_count) => (append acc [(x_count, y_count)], (y_count+1))) ([], 1) 10 + in (append acc list, (x_count+1)) + end) ([], 1) 10 + val c_h = foldl (fn(x,y) => remove_elem_xs x y) init [7, 8, 9, 10] + val c_v = foldl (fn(x,y) => remove_elem_ys x y) init [7, 8, 9, 10] + val b_h = foldl (fn(x,y) => remove_elem_xs x y) init [8, 9, 10] + val b_v = foldl (fn(x,y) => remove_elem_ys x y) init [8, 9, 10] + val s_h = foldl (fn(x,y) => remove_elem_xs x y) init [9, 10] + val s_v = foldl (fn(x,y) => remove_elem_ys x y) init [9, 10] + val d_h = foldl (fn(x,y) => remove_elem_xs x y) init [10] + val d_v = foldl (fn(x,y) => remove_elem_ys x y) init [10] + in {c_h, c_v, b_h, b_v, s_h, s_v, d_h, d_v} + end + + + fun board_ships_gen tco size = + let val init_avail = make_init_avail_rec () + val (carrier, avail1) = ship_gen init_avail "C" tco size + val (battleshp, avail2) = ship_gen avail1 "B" tco size + val (sub1, avail3) = ship_gen avail2 "S" tco size + val (sub2, avail4) = ship_gen avail3 "S" tco size + val (destroyer, _) = ship_gen avail4 "D" tco size + val ship_ls = [carrier, battleshp, sub1, sub2, destroyer] + val (board, ships) = make_board ship_ls + in + (board, ships) + end + + fun attack_gen tco size = + let val res = (integer(1, 10) tco size, integer(1,10) tco size) + in + res + end + + fun test_do_attack_no_leak (board, ships) attack = + let val interim_res1 = ((levelOf board) = (levelOf ships)) + val interim_res2 = ((levelOf board) = (levelOf (do_attack board ships attack))) + in (interim_res1 andalso interim_res2) + end + + fun random_labels_gen val_gen tco size = + let val labels = list(label()) tco size + val res = combined_labeled_value (labels, val_gen) tco size + in res + end + + fun test_bad_do_attack (board, ships) attack = + (length (do_attack board ships attack).1) = 11 + + fun prop_do_att_test() = + for_all ([(random_labels_gen board_ships_gen), attack_gen], test_do_attack_no_leak) + + fun prop_bad_do_att() = + for_all ([(labeled_value ([`{alice}`, `{bob}`], board_ships_gen)), attack_gen], test_bad_do_attack) + +in setup () 0 +end \ No newline at end of file diff --git a/troupecheck/battleship/battleship-player.trp b/troupecheck/battleship/battleship-player.trp new file mode 100644 index 0000000..b4c7014 --- /dev/null +++ b/troupecheck/battleship/battleship-player.trp @@ -0,0 +1,154 @@ +import lists +import stdio +let fun write x = + fwrite ((getStdout authority), x) + + fun print_board b = + write "\n"; + foldl (fn (x,_) => foldl (fn (y,_) => write (" "^y^" ")) () x; write "\n")() b + + fun make_row (f, i) = + case i of + 0 => [] + | _ => append (make_row (f, i-1)) [f i] + + fun bound_from_ship ship = + case ship of + "C" => 5 + | "B" => 4 + | "S" => 3 + | "D" => 2 + + fun update_board board_or_error coordinate = + case getType board_or_error of + "string" => board_or_error + | _ => + let fun place_horizontal (x, y) ship_type board = + let val y_ls = nth board y + val upperbound = x + (bound_from_ship ship_type) + val is_valid = (x >= 1) andalso (upperbound <= 11) + in if is_valid then + let val new_y = make_row ((fn i => if (i >= x) andalso (i < upperbound) then ship_type else (nth y_ls i)), 10) + val new_board = make_row ((fn i => if i = y then new_y else (nth board i)), 10) + in new_board + end + else + ("Invalid coordinates for ship of type: " ^ ship_type) + end + + fun place_vertical (x, y) ship_type board = + let val upperbound = y + (bound_from_ship ship_type) + val is_valid = (x >= 1) andalso (upperbound <= 11) + in if is_valid then + let val new_board = make_row ((fn i => + if i >= y andalso i < upperbound then + make_row ((fn j => if j = x then ship_type else nth (nth board i) j), 10) + else nth board i), 10) + in new_board + end + else + ("Invalid coordinates for ship of type: " ^ ship_type) + end + val ((x,y), direction, ship) = coordinate + in case direction of + "v" => place_vertical (x,y) ship board_or_error + | "h" => place_horizontal (x,y) ship board_or_error + end + + fun for_i body acc 0 = acc.0 + | for_i body acc to = for_i body (body acc) (to-1) + + fun ship_coords_from_info info = + let val (org_x, org_y) = info.0 + val count = (bound_from_ship info.2)-1 + in case info.1 of + "h" => + let val coords = for_i (fn acc => (append acc.0 [((acc.1)+1, org_y)], (acc.1)+1)) ([info.0], org_x) count + in coords + end + |"v" => + let val coords = for_i (fn acc => (append acc.0 [(org_x, (acc.1)+1)], (acc.1)+1)) ([info.0], org_y) count + in coords + end + end + + + fun make_board ls = + let val start_board = make_row ((fn _ => make_row ((fn _ => "-"), 10)), 10) + val (board, ships) = foldl (fn (x,(board_acc, ships_acc)) => (update_board board_acc x, append ships_acc [ship_coords_from_info x])) (start_board, []) ls + in (board, ships) + end + + + val c1 = ((3,2), "h", "C") + val c2 = ((2,3), "v", "S") + val c3 = ((8,9), "h", "D") + val c4 = ((3,5), "v", "B") + val c5 = ((8,3), "h", "D") + + fun player() = + receive [hn ("STARTING", player_num) => + let val _ = write "\nBoth players have joined. Player 1 starts.\n" + val _ = write ("\nYou are player " ^ (toString player_num) ^ ".\n") + in player() + end, + + hn ("YOURTURN", senderid) => + let val _ = write "\nPlease pick x-coordinate of attack: \n>" + val x_attack = inputLineAtLevel authority `{}` + val _ = write "\nPlease pick y-coordinate of attack: \n>" + val y_attack = inputLineAtLevel authority `{}` + val (x, y) = (stringToInt(x_attack), stringToInt(y_attack)) + val _ = send(senderid, (("ATTACK", (x,y)), self())) + in player() + end, + + hn (("ATTACK_RESP", msg), senderid) => + case msg of + "Illegal coordinate" => + let val _ = write ("\nIllegal attack coordinate! Try with another coordinate...\n") + in player() + end + |_ => + let val _ = write ("\nYour move was a " ^ msg ^ "!") + val _ = write ("\nWaiting for opponent to attack...\n") + in player () + end, + + hn ("UPDATE_MSG", coords, msg, new_board) => + let val _ = write ("\nOpponent attacked (" ^ (toString coords.0) ^ ", " ^ (toString coords.1) ^").") + in case msg of + "Illegal coordinate" => + let val _ = write ("\nThis is an illegal attack coordinate! Wait for opponent to try again...\n") + in player() + end + |_ => + let val _ = print_board new_board + val _ = write ("\nThis move was a " ^ msg ^ "!") + val _ = write ("\nIt is now your turn.\n") + in player() + end + end, + + hn "YOUWON" => + let val _ = write ("\nCongratulations! You sank all the opponent's ships. You are the Winner!\n") + in exit (authority, 0) + end, + + hn ("YOULOST", new_board, coords) => + let val _ = write ("\nOpponent attacked (" ^ (toString coords.0) ^ ", " ^ (toString coords.1) ^").") + val _ = print_board new_board + val _ = write ("\nToo bad! The opponent sank all your ships. You lost...\n") + in exit (authority, 0) + end + ] + + fun join() = + let val (board, ships) = make_board [c1,c2,c3,c4, c5] + val game = whereis ("@battleship-game", "battleship") + val _ = send(game, ("JOINING", board, ships, self())) + in player() + end + +in join() +end \ No newline at end of file diff --git a/troupecheck/battleship/ids/battleship-game.json b/troupecheck/battleship/ids/battleship-game.json new file mode 100644 index 0000000..a0133f8 --- /dev/null +++ b/troupecheck/battleship/ids/battleship-game.json @@ -0,0 +1 @@ +{"id":"12D3KooWLz6JNygFFtyTjujjU29ivACgp9bxYGCHheoyfwxpgpv7","privKey":"CAESQHzfORXAw9jg1Orw0QnFl7xQZih3VCrcDXMgW+mgXFxbpe5r/80tddCxZVNjofJTk47pqn2Jq5rIbhtWLAiDdYw=","pubKey":"CAESIKXua//NLXXQsWVTY6HyU5OO6ap9iauayG4bViwIg3WM"} \ No newline at end of file diff --git a/troupecheck/battleship/ids/battleship-player1.json b/troupecheck/battleship/ids/battleship-player1.json new file mode 100644 index 0000000..ed2454e --- /dev/null +++ b/troupecheck/battleship/ids/battleship-player1.json @@ -0,0 +1 @@ +{"id":"12D3KooWCCB5cy5eYhdrzPqUqYbmcQjKiKjBA8EH3jvtP5R6jkxc","privKey":"CAESQIVYFeWVRwsLSKymg6z+FzoNveYRo19ERFdki4P8GxZUI02dMRgIJkdHC10Wfe0ihkVhHixN0fFLwAW/WN7L4YU=","pubKey":"CAESICNNnTEYCCZHRwtdFn3tIoZFYR4sTdHxS8AFv1jey+GF"} \ No newline at end of file diff --git a/troupecheck/battleship/ids/battleship-player2.json b/troupecheck/battleship/ids/battleship-player2.json new file mode 100644 index 0000000..6d7769a --- /dev/null +++ b/troupecheck/battleship/ids/battleship-player2.json @@ -0,0 +1 @@ +{"id":"12D3KooWQwT7Pv3vVTZjkhztwU4zzp3mNMQSstzkN2vvNai4uqNv","privKey":"CAESQIw7wMQo9IIb0d4cxLEDQIEPq+rtO3enBQp+ukOtP1Ez4K/1MjIIUEC1afWig9nWdspiw2fpp9GuSGgJcBlRZ2c=","pubKey":"CAESIOCv9TIyCFBAtWn1ooPZ1nbKYsNn6afRrkhoCXAZUWdn"} \ No newline at end of file diff --git a/troupecheck/language-interpreter/test-language.trp b/troupecheck/language-interpreter/test-language.trp new file mode 100644 index 0000000..64991f8 --- /dev/null +++ b/troupecheck/language-interpreter/test-language.trp @@ -0,0 +1,179 @@ +import troupecheck +import lists +(* +-------------------------------- +CUSTOM TYPE PROGRAM + +Used for testing the creation of complex custom generators. +Here we defined an interpreter and generator for simple programs consisting of: +expr := ("num", number) |("var", string) |("add", expr, expr) |("sub", expr, expr) |("mul", expr, expr) |("div", expr, expr) +stmt := ("assign", string, expr) |("print", expr) +prog := [[stmt], expr] + +-------------------------------- +*) +let fun eval exp env = + case exp of + ("num", n) => n + | ("var", n) => lookup env n ("unknown variable " ^ n) + | ("add", e1, e2) => (eval e1 env) + (eval e2 env) + | ("sub", e1, e2) => (eval e1 env) - (eval e2 env) + | ("mul", e1, e2) => (eval e1 env) * (eval e2 env) + | ("div", e1, e2) => (eval e1 env) / (eval e2 env) + | _ => print ("Error: ill defined expression"); exit (authority, 1) + + fun execute stmt env = + case stmt of + ("assign", var, exp) => + let val value = eval exp env + in + append [(var, value)] env + end + | ("print", exp) => (()(* print ("from prog: " ^ (toString (eval exp env)) *); env) + + fun remove_nth n [] i = [] + | remove_nth n (x::xs) i = + if n = i then xs + else x :: (remove_nth n xs (i + 1)) + + fun interpret prog = + let fun interpretHelper [] env = env + | interpretHelper (stmt :: rest) env = + let val newEnv = execute stmt env + in + interpretHelper rest newEnv + end + val (stmts, exp) = prog + val last_env = (interpretHelper stmts []) + in + eval exp last_env + end + + fun optimize_prog prog = + let val (stmts, exp) = prog + fun optimize_exp exp = + case exp of + ("num", n) => ("num", n) + | ("var", x) => ("var", x) + | ("add", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1+n2)) + |_ => ("add", (optimize_exp e1), (optimize_exp e2))) + | _ => ("add", (optimize_exp e1), (optimize_exp e2))) + | ("sub", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1-n2)) + |_ => ("sub", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("sub", (optimize_exp e1), (optimize_exp e2))) + | ("mul", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1*n2)) + |_ => ("mul", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("mul", (optimize_exp e1), (optimize_exp e2))) + | ("div", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => if ((n1 = 0) andalso (n2 = 0)) then ("div", e1, e2) else ("num", (n1/n2)) + |_ => ("div", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("div", (optimize_exp e1), (optimize_exp e2))) + + fun optimize_stmt stmt = + case stmt of + ("assign", var, exp) => ("assign", var, (optimize_exp exp)) + | ("print", exp) => ("print", (optimize_exp exp)) + in + ((map optimize_stmt stmts), optimize_exp exp) + end + + fun exp_gen ls nesting_level tco size = + let val exp_ts = + if nesting_level = 2 then ["num"] + else (if length ls = 0 then ["num", "add", "sub", "mul", "div"] + else ["var", "num", "add", "sub", "mul", "div"]) + val exp_type = one_of exp_ts tco size + in + case exp_type of + "num" => + let val value = integer(1, inf) tco size in + ("num", value) end + | "var" => + let val value = one_of ls tco size in + ("var", value) end + |"add" => + let val e1 = exp_gen ls (nesting_level+1) tco size + val e2 = exp_gen ls (nesting_level+1) tco size + in + ("add", e1, e2) + end + |"sub" => + let val e1 = exp_gen ls (nesting_level+1) tco size + val e2 = exp_gen ls (nesting_level+1) tco size + in + ("sub", e1, e2) + end + |"mul" => + let val e1 = exp_gen ls (nesting_level+1) tco size + val e2 = exp_gen ls (nesting_level+1) tco size + in + ("mul", e1, e2) + end + |"div" => + let val e1 = exp_gen ls (nesting_level+1) tco size + val e2 = exp_gen ls (nesting_level+1) tco size + in + ("div", e1, e2) + end + end + + fun assign_stmt_gen ls tco size = + let val n = string() tco size + val exp = exp_gen ls 0 tco size + in + ("assign", n, exp) + end + + fun print_stmt_gen ls tco size = + let val exp = exp_gen ls 0 tco size + in + ("print", exp) + end + + fun stmt_gen ls tco size = + let val stmt = one_of ["print", "assign"] tco size + in + case stmt of + "assign" => + let val res = assign_stmt_gen ls tco size in + res end + |"print" => + let val res = print_stmt_gen ls tco size in + res end + end + + fun program_gen tco size = + let val num_of_insts = (integer(0, size) tco size) + fun prog_gen_aux env p 0 = (p, env) + | prog_gen_aux env p i = + let val stmt = stmt_gen env tco size + val newEnv = if stmt.0 = "assign" then (append [stmt.1] env) else env + in + prog_gen_aux newEnv (append p [stmt]) (i-1) + end + val (prog_stmts, last_env) = prog_gen_aux [] [] num_of_insts + val last_exp = exp_gen last_env 0 tco size + val prog = (prog_stmts, last_exp) + in + prog + end + + fun test_prog_opt prog = + (interpret prog) = (interpret (optimize_prog prog)) + fun test_prog_shrink prog = + (interpret prog) < 100 + fun prop_program_shrink() = for_all ([program_gen], test_prog_shrink) + fun prop_program_opt() = for_all ([program_gen], test_prog_opt) +in troupecheck [prop_program_opt, prop_program_shrink] authority +end \ No newline at end of file diff --git a/troupecheck/tc_archive/tc_ext_shrink.trp b/troupecheck/tc_archive/tc_ext_shrink.trp new file mode 100644 index 0000000..85d00e4 --- /dev/null +++ b/troupecheck/tc_archive/tc_ext_shrink.trp @@ -0,0 +1,1124 @@ +import lists +(* +-------------------------------- +PRINTING TO CONSOLE - q +-------------------------------- +*) +let val out = getStdout authority + fun write x = fwrite (out, x) + (* arguments are always in a list - for easier readability these are removed when converting arguments to string *) + fun args_toString args = + let fun aux_toString acc (x0::x1::xs) = aux_toString (acc ^ (toString x0) ^ ", ") (x1::xs) + | aux_toString acc (x::xs) = acc ^ (toString x) in + aux_toString "" args end + + fun nth (x::l) 1 = x + | nth (x::l) n = nth l (n - 1) + | nth x y = print x; print y; exit (authority, 0) +(* +-------------------------------- +ERROR HANDLING - w +-------------------------------- +*) + fun report_error error_reason = + write "\u001B[31m \nError: "; (* Changing the print color to red *) + let val err_string = case error_reason of + ("cant_generate", tries) => "Couldn't produce an instance that satisfies all strict constraints after " + ^ (toString tries) ^ " tries.\n" + | ("cant_satisfy", tries) => "No valid test could be generated after " ^ (toString tries) ^ " tries.\n" + | ("non_boolean_result", _) => "The property or precondition code returned a non-boolean result.\n" + | ("type_mismatch", _) => "The types' structure doesn't match the property.\n" + | ("illegal_gen_def", _ ) => "Generator is defined wrong - use tuple() or record() to combine generators.\n" + | ("record_mismatch", _) => "the number of names provided for record generation, does not match the number of types provided.\n" + | ("shrinking_looped", _) => "Shrinking looped.\n" + | ("non_string_type", _) => "An element of non-string type found when trying to convert list to string.\n" + in + write (err_string ^ "\u001B[0m"); (* Changing the color back *) + exit (authority, 0) end + + fun boolean_check x = + if (getType x)<>"boolean" then report_error ("non_boolean_result", 0) else () + + fun function_not_done_check p = + if (getType p)<>"function" then report_error ("type_mismatch", 0) else () +(* +-------------------------------- +UTILS - e +-------------------------------- +*) + fun remove_nth n [] i = [] + | remove_nth n (x::xs) i = + if n = i then xs + else x :: (remove_nth n xs (i + 1)) + + fun make_list (f, i) = + case i of + 0 => [] + | _ => append [f()] (make_list (f, i-1)) + + fun abs_value x = + if x < 0 then -x else x + +(* applies the list of arguments to the property - one by one - reporting errors along the way *) +(* TODO: handle when arguments are passed to a property that does not take arguments *) + fun apply_args p l = + case l of + [] => boolean_check (p()); p() (* this case is only reached if there are no generators to beign with*) + | (x::xs) => + let val res = foldl (fn (x,y) => function_not_done_check y; y x) p l in + boolean_check res; + res + end + + fun string_to_list s = + let fun aux "" acc = acc + | aux s acc = + let val x = substring (s, 0, 1) + val xs = substring (s, 1, 1/0) in + aux xs (append acc [x]) end in + aux s [] end + + fun list_to_string ls = + foldl (fn (x,y) => if getType x <> "string" then report_error ("non_string_type", 0) else y ^ x) "" ls + + fun string_length s = + length (string_to_list s) + + fun report_fail_reason rec noOfTests= + case rec.failReason of + "false_prop" => + write "\nFailure at input: "; + write (args_toString (map (fn x => x.raw) rec.cEx)); + write ("\nAfter running: " ^ (toString (noOfTests - rec.remTests + 1)) ^ " test(s)\n") + + fun build_record names vals = + let fun aux r [] [] = r + | aux r (n::ns) (v::vs) = + aux (recordExtend(r, n, v)) ns vs in + aux {} names vals + end + + fun build_tuple ls = + case ls of + [] => (0) + |[x] => (x) + |[x1,x2] => (x1,x2) + |[x1,x2,x3] => (x1,x2,x3) + |[x1,x2,x3,x4] => (x1,x2,x3,x4) + |[x1,x2,x3,x4,x5] => (x1,x2,x3,x4,x5) + |[x1,x2,x3,x4,x5,x6] => (x1,x2,x3,x4,x5,x6) + |[x1,x2,x3,x4,x5,x6,x7] => (x1,x2,x3,x4,x5,x6,x7) + |[x1,x2,x3,x4,x5,x6,x7,x8] => (x1,x2,x3,x4,x5,x6,x7,x8) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9] => (x1,x2,x3,x4,x5,x6,x7,x8,x9) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10] => (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) + |_ => (2, 3, 4, 5) +(* +-------------------------------- +SHRINKING - r +-------------------------------- +*) + + and shrink_float rec = + let val rec_checked = if rec.curr = 0 then {rec with state = "done"} else rec + val curr_val = rec_checked.curr + in + case rec_checked.state of + "rollback" => + {state = "done", curr = rec_checked.prev, prev = rec_checked.curr} + |"done" => + rec_checked + | _ => + let val new_raw_val = if (abs_value curr_val)-1 <= 0 then 0 else curr_val-1 + in + {state = "cont", curr = new_raw_val, prev = rec_checked.curr} + end + end + + and shrink_int rec = + let val interim = shrink_float rec + in + {interim with curr = floor(interim.curr)} + end + + and shrink_bool rec = + let val rec_checked = if rec.curr = false then {rec with state = "done"} else rec + in + case rec_checked.state of + "rollback" => + {state = "done", curr = rec_checked.prev, prev = rec_checked.curr} + |"done" => + rec_checked + | _ => + let val newVal = false + in + {state = "cont", curr = newVal, prev = rec_checked.curr} + end + end + + (* input/returns - {state: string, curr: string, prev: string} *) + and shrink_string rec = + let val rec_checked = if rec.state = "init" then {rec with next_shrink_info = 0} else rec in + case rec_checked.state of + "cont_elem" => + {rec_checked with state = "done"} (* TODO: Should actually shrink characters *) + | _ => + let val ls_curr = string_to_list rec_checked.curr + val ls_prev = string_to_list rec_checked.prev + val shrinkers = map (fn _ => shrink_char) ls_curr + val interim_res = + shrink_list shrinkers {state = rec_checked.state, + curr = ls_curr, + prev = ls_prev, + idx = rec_checked.next_shrink_info, + shrinkers = shrinkers, + prev_shrinkers = shrinkers} + val new_curr = list_to_string interim_res.curr + val new_prev = list_to_string interim_res.prev + + val res = {state = interim_res.state, curr = new_curr, prev = new_prev, next_shrink_info = interim_res.idx} + in + res + end + end + + and shrink_char rec = + let val chars = + ["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", + "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", + "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", + "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", + "0", "1", "2", "3", "4", "5", "6", "7", "8", "9"] + val rec_checked = if rec.curr = "a" then {rec with state = "done"} else rec + val curr_val = rec_checked.curr in + case rec_checked.state of + "rollback" => + {state = "done", curr = rec.prev, prev = rec.curr, idx = rec.idx} + | "done" => + rec_checked + | "init" => + let val index_of_new = (lookup chars rec.curr 2) - 1 + val new_char = nth chars index_of_new + in + {state = "cont", curr = new_char, prev = rec.curr, idx = index_of_new} + end + | _ => + let val index_of_new = rec.idx-1 + val new_char = nth chars index_of_new + in + {state = "cont", curr = new_char, prev = rec.curr, idx = index_of_new} + end + end + + and shrink_sized_aggregate vals builder rec = + case rec.state of + "init" => + let val init_shrink_idx = 0 + val new_vals = mapi (fn (i, x) => + if i = init_shrink_idx then (x.shrinker {state = "init", curr = x.raw, prev = x.raw}) + else {state = "init", curr = x.raw, prev = x.raw}) vals + val new_raw_vals = map (fn x => x.curr) new_vals + val new_state = if (foldl (fn (x,y) => (x.state = "done") andalso y) true new_vals) then "done" else "cont" + val shrink_idx = if (nth new_vals (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + in + {state = new_state, curr = (builder new_raw_vals), prev = rec.curr, next_shrink_info = new_vals, shrink_idx = shrink_idx} + end + | "cont" => + let val init_shrink_idx = rec.shrink_idx + val new_vals = mapi (fn (i, x) => + if i = init_shrink_idx then x.shrinker (nth rec.next_shrink_info (i+1)) + else (nth rec.next_shrink_info (i+1))) vals + val new_raw_vals = map (fn x => x.curr) new_vals + val new_state = if (foldl (fn (x,y) => (x.state = "done") andalso y) true new_vals) then "done" else "cont" + val shrink_idx = if (nth new_vals (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + in + {state = new_state, curr = (builder new_raw_vals), prev = rec.curr, next_shrink_info = new_vals, shrink_idx = shrink_idx} + end + | "done" => + rec + | "rollback" => + let val init_shrink_idx = rec.shrink_idx + fun rollback_aux (i, x) = + if i = init_shrink_idx then + (let val val_to_shrink = {(nth rec.next_shrink_info (i+1)) with state = "rollback"} + in + x.shrinker val_to_shrink + end ) + else (nth rec.next_shrink_info (i+1)) + val rollback_args = mapi rollback_aux vals + val new_raw_vals = map (fn x => x.curr) rollback_args + val new_state = if (foldl (fn (x,y) => (x.state = "done") andalso y) true rollback_args) then "done" else "cont" + val shrink_idx = if (nth rollback_args (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + in + {state = new_state, curr = (builder new_raw_vals), prev = rec.curr, next_shrink_info = rollback_args, shrink_idx = shrink_idx} + end + + and shrink_list shrinkers rec = + if (rec.curr = []) andalso (rec.state <> "rollback") then {rec with state = "done", prev = rec.curr, idx = 0} + else + case rec.state of + "init" => + let val removeIdx = (length (rec.curr)) - 1 + val newList = remove_nth removeIdx rec.curr 0 + val new_shrinkers = remove_nth removeIdx shrinkers 0 + val next_state = if length newList = 0 then "cont_elem" else "cont_size" + in + {state = next_state, curr = newList, prev = rec.curr, idx = removeIdx, shrinkers = new_shrinkers, prev_shrinkers = shrinkers} + end + | "cont_size" => + let val remove_idx = (rec.idx - 1) + val next_state = if remove_idx <= 0 then "cont_elem" else "cont_size" + val new_list = remove_nth remove_idx rec.curr 0 + val new_shrinkers = remove_nth remove_idx rec.shrinkers 0 + in + {state = next_state, curr = new_list, prev = rec.curr, idx = remove_idx, shrinkers = new_shrinkers, prev_shrinkers = rec.shrinkers} + end + | "cont_elem" => + let val interim_list = mapi (fn (i, x) => (nth rec.shrinkers (i+1)){state = "init", curr = x, prev = x}) rec.curr + val next_state = if (foldl (fn (x,y) => (x.state = "done") andalso y) true interim_list) then "done" else "cont_elem" + val new_list = map (fn x => x.curr) interim_list + in + {state = next_state, curr = new_list, prev = rec.curr, idx = rec.idx, shrinkers = rec.shrinkers, prev_shrinkers = rec.prev_shrinkers} + end + | "rollback" => + if (length rec.curr) = (length rec.prev) then + {state = "done", curr = rec.prev, prev = rec.curr, idx = rec.idx, shrinkers = rec.prev_shrinkers, prev_shrinkers = rec.shrinkers} (* TODO: this loops an unecesary amount of times *) + else + {state = "cont_size", curr = rec.prev, prev = rec.curr, idx = rec.idx, shrinkers = rec.prev_shrinkers, prev_shrinkers = rec.shrinkers} + | "done" => + rec + + and args_shrink args = + case args.state of + "rollback" => + let val init_shrink_idx = args.shrink_idx + val rollbackReadyArgs = mapi (fn (i, x) => if (x.state = "done") orelse (i<>init_shrink_idx) then x else {x with state = "rollback"}) args.args + val argsRolledBack = mapi (fn (i, x) => if i = init_shrink_idx then (nth args.shrinkers (i+1)) x else x) rollbackReadyArgs + val nextState = if (foldl (fn (x,y) => (x.state = "done") andalso y) true argsRolledBack) then "done" else "cont" + val shrink_idx = if (nth argsRolledBack (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + in + {state = nextState, args = argsRolledBack, shrinkers = args.shrinkers, shrink_idx = shrink_idx} + end + | "done" => + args + | _ => + let val init_shrink_idx = args.shrink_idx + val newArgs = mapi (fn (i, x) => if i = init_shrink_idx then (nth args.shrinkers (i+1)) x else x) args.args + val nextState = if (foldl (fn (x,y) => (x.state = "done") andalso y) true newArgs) then "done" else "cont" + val shrink_idx = if (nth newArgs (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + + in + {state = nextState, args = newArgs, shrinkers = args.shrinkers, shrink_idx = shrink_idx} + end + + fun shrink_aux args prop pre counter = + if counter = 1000 then report_error ("shrinking_looped", 0) else + let val shrunk_args = args_shrink args + val shrunk_args_raw = map (fn x => x.curr) shrunk_args.args + val precond_is_met = if (pre <> ()) then (apply_args pre shrunk_args_raw) else true in + case (apply_args prop shrunk_args_raw) orelse (precond_is_met = false) of + true => shrink_aux (args_shrink {state = "rollback", args = shrunk_args.args, shrinkers = args.shrinkers, shrink_idx = args.shrink_idx}) prop pre (counter) + | false => + if shrunk_args.state = "done" then {shrunk_ctx = shrunk_args_raw, count = counter} else shrink_aux shrunk_args prop pre (counter+1) end + + fun shrink args prop pre = + let val start_time = getTime() + val shrinkers = map (fn x => x.shrinker) args + val args_shrink_ready = map (fn x => {state = "init", curr = x.raw, prev = x.raw}) args + val args_rec = {state = "init", args = args_shrink_ready, shrinkers = shrinkers, shrink_idx = 0} + val res = shrink_aux args_rec prop pre 0 + val end_time = getTime() + in (res, (end_time - start_time)) end +(* +-------------------------------- +GENERATORS - t +-------------------------------- +*) + (* return - {raw: bool, shrinker: fn {state: string, curr: bool, prev: bool} => ..: {state: string, curr: bool, prev: bool}} *) + fun bool_gen size = + let val rnd = random() + val res = if rnd < 1/2 then false + else true + in + {raw = res, shrinker = shrink_bool} + end + + (* return - {raw: number, shrinker: fn {state: string, curr: number, prev: number} => ..: {state: string, curr: number, prev: number}} *) + (* TODO: Fix shrinking towards zero -> should shrink towards lowest valid val *) + fun float_gen (low, high) size = + let val x = random() + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + val raw_res = + case (lInf, hInf) of + (true, true) => if (bool_gen size).raw then x*size else -x*size + | (true, false) => high - (x*size) + | (false, true) => low + (x*size) + | (false, false) => low + (x * (high-low)) + in + {raw = raw_res, shrinker = shrink_float} + end + + (* return - {raw: number, shrinker: fn {state: string, curr: number, prev: number} => ..: {state: string, curr: number, prev: number}} *) + fun int_gen (low, high) size = + let val raw_res = floor ((float_gen(low, high+1) size).raw) + in + {raw = raw_res, shrinker = shrink_int} + end + + (* return - {raw: list, shrinker: fn {state: string, curr: list, prev: list} => ..: {state: string, curr: list, prev: list}} *) + fun list_gen (generator) size = + let val length = (int_gen(0, size) size).raw + val res = make_list ((fn () => generator size), length) + val raw_res = map (fn x => x.raw) res + val shrinkers = map (fn x => x.shrinker) res in + {raw = raw_res, shrinker = shrink_list shrinkers} + end + + (* NOTE: Generates only letters (upper and lower case) and numbers. *) + (* return - {raw: char, shrinker: fn {state: string, curr: char, prev: char} => ..: {state: string, curr: char, prev: char}} *) + fun char_gen size = + let val chars = + ["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", + "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", + "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", + "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", + "0", "1", "2", "3", "4", "5", "6", "7", "8", "9"] + val x = (int_gen (1, ((length chars)-1)) size).raw + in + {raw = (nth chars x), shrinker = shrink_char} + end + +(* NOTE: Generates only strings of letters (upper and lower case) and numbers. *) + (* return - {raw: string, shrinker: fn {state: string, curr: string, prev: string} => ..: {state: string, curr: string, prev: string}} *) + fun string_gen size = + let val x = (int_gen (0, size) size).raw + fun fold f acc 0 = acc + | fold f acc i = fold f (acc ^ (f())) (i-1) + val raw_string = (fold (fn () => (char_gen x).raw) "" x) + in + {raw = raw_string, shrinker = shrink_string} + end + +(* NOTE: Hardcoded for tuple of up to 10 elements *) +(* returns a record with raw_inst: a tuple of whatever values specified, and meta_data is a list + of all generated values in raw_inst along with their respective meta_data. *) + fun tuple_gen ts size = + let val ts_vals = map (fn x => x size) ts + val ts_raw_vals = map (fn x => x.raw) ts_vals + val ts_shrinkers = map (fn x => x.shrinker) ts_vals + in + {raw = (build_tuple ts_raw_vals), shrinker = shrink_sized_aggregate ts_vals build_tuple} + end + +(* +ns: list of strings - will be used as fieldnames +ts: list of generators - used to generate values for fields + +Returns record: {raw_inst = <>, meta_data = (ns, <>)} +*) + fun rec_gen ns ts size = + if (length ns) <> (length ts) then + report_error ("record_mismatch", 0) + else + let val ts_vals = map (fn x => x size) ts + val ts_raw_vals = map (fn x => x.raw) ts_vals + val raw_res = build_record ns ts_raw_vals + in + {raw = raw_res, shrinker = shrink_sized_aggregate ts_vals (build_record ns)} + end + + + fun generator_gen size = + let val rnd = random() + val inf = 1/0 + val res = if rnd <= 1/7 then ((fn i => int_gen(inf, inf) i)) else + if rnd <= 2/7 then ((fn i => bool_gen i)) else + if rnd <= 3/7 then ((fn i => float_gen(inf, inf) i)) else + if rnd <= 4/7 then ((fn i => string_gen i)) else + if rnd <= 5/7 then ((fn i => char_gen i)) else + if rnd <= 6/7 then ((fn i => tuple_gen (make_list ((fn () => int_gen(inf, inf)), i)) i)) else + ((fn i => list_gen (int_gen(inf, inf)) i)) in + res end + +(* +-------------------------------- +CORE FUNCTIONALITY - a +-------------------------------- +*) + fun core_forall (generator, prop, 0, size, pre, cap) = {failReason = (), cEx = (), remTests = 0} + |core_forall (generator, prop, i, size, pre, cap) = + let val args = map (fn x => x size) generator + val raw_args = map (fn x => x.raw) args in + case pre of + () => + if (apply_args prop raw_args) then (write "."; core_forall (generator, prop, i-1, size+1, pre, cap)) + else (write "!"; {failReason = "false_prop", cEx = args, remTests = i}) + | _ => + if (apply_args pre raw_args) then + if (apply_args prop raw_args) then (write "."; core_forall (generator, prop, i-1, size+1, pre, cap)) + else (write "!"; {failReason = "false_prop", cEx = args, remTests = i}) + else + (write "x"; + if (size = cap) andalso (i*5 = cap) then report_error ("cant_satisfy", size) + else if size = cap then {failReason = (), cEx = (), remTests = i} + else core_forall (generator, prop, i, size+1, pre, cap)) + end + + fun run_tests generators p noOfTests = + let val (prop, pre) = + case p of + (x,y) => (x,y) + | x => (x, ()) + val res = core_forall (generators, prop, noOfTests, 0, pre, (noOfTests*5)) in + case res.failReason of + () => write ("\u001B[1m \u001B[32m \nSuccess: \u001B[0mPassed all " ^ (toString noOfTests) ^ " test(s).\n"); true + |_ => + report_fail_reason res noOfTests; + write ("\u001B[1m\u001B[34mShrinking\u001B[0m:"); + (* let val shrink_res = shrink res.cEx prop pre in + write "\nFailing test case was shrunk to:\n"; + write (args_toString shrink_res.shrunk_ctx); + write ("\nAfter " ^ (toString shrink_res.count) ^ " iterations.\n"); *) + (false, res.cEx) + (* end *) + end + + fun for_all (generators, p) = run_tests generators p 100 + | for_all (generators, p, noOfTests) = run_tests generators p noOfTests + + fun troupecheck props = + let val n = toString (length props) + fun troupecheck_aux [] acc i = acc + | troupecheck_aux (x::xs) acc i = + let val _ = write ("\nRunning test " ^ (toString i) ^ " of " ^ n ^ ":\n") + val res = x() + in troupecheck_aux xs res (i+1) end + in troupecheck_aux props () 1 + end + +(* +-------------------------------- +CONVENIENCE FUNCTIONS - s +-------------------------------- +*) + val inf = 1 / 0 + fun integer() = int_gen(inf, inf) + | integer (h, l) = int_gen(h, l) + + fun pos_integer() = integer(0, inf) + + fun neg_integer() = integer(inf, -1) + + fun float() = float_gen(inf, inf) + | float(h, l) = float_gen(h, l) + + fun pos_float() = float(0, inf) + + fun neg_float() = float(inf, 0) + + fun boolean() = bool_gen + + fun list() = list_gen(generator_gen()) (* TODO: generator_gen() should return both raw_gen and meta_data *) + |list(type) = list_gen(type) + + fun string() = string_gen + + fun char() = char_gen + + fun tuple ts = tuple_gen ts + + fun record ns ts = rec_gen ns ts + + fun one_of ls size = + let val {raw, shrinker} = (int_gen (1, (length ls)) ((length ls))) + val raw_res = nth ls raw + fun oneOf_shrinker inst = + case inst.state of + "init" => + let val interim = shrinker {state = inst.state, curr = raw, prev = raw} + val new_idx = if interim.curr < 1 then 1 else interim.curr + val _ = print new_idx + val _ = print ls + val new_pick = nth ls new_idx + in {state = interim.state, curr = new_pick, prev = inst.curr, idx = new_idx, prev_idx = raw} + end + | _ => + if inst.idx = 1 then {inst with state = "done"} + else + let val interim = shrinker {state = inst.state, curr = inst.idx, prev = inst.prev_idx} + val new_idx = if interim.curr < 1 then 1 else interim.curr + val _ = print new_idx + val _ = print ls + val new_pick = nth ls new_idx + in {state = interim.state, curr = new_pick, prev = inst.curr, idx = new_idx, prev_idx = inst.idx} + end + in + {raw = raw_res, shrinker = oneOf_shrinker} + end +(* +-------------------------------- +FUNCTIONS FOR TESTING - d +-------------------------------- +*) + fun my_reverse xs = + xs + + fun my_floor i = + if i >=0 then i - (i mod 1) + else i - (i mod 1) - 1 + + fun my_length [] = 0 + | my_length (x::xs) = 1 + (my_length xs) + + fun my_count y [] = 0 + | my_count y (x::xs) = + let val z = + if y = x then 1 else 0 + in + z + my_count y xs end + + fun my_floor i = + if i >=0 then i - (i mod 1) + else i - (i mod 1) - 1 + + fun my_ceil_1 i = + if i > 0 then i + (1 - (i mod 1)) + else i + (1 - (i mod 1)) - 1 + + fun my_ceil_2 i = + if i > 0 then (my_floor i) + 1 + else if i = 0 then 0 + else (my_floor i) + 1 + + fun bad_insert xs x = + if length xs < 10 then append [x] xs else + xs + + fun one_of_two (x, y) = + let val bool = (bool_gen 0).raw in + if bool then x + else y end + + fun bad_half n = + if n > 10 then n else n/2 + + fun lengths_not_same s1 s2 = + (string_length s1) <> (string_length s2) + +(* +-------------------------------- +PROPERTIES FOR TESTING - f +-------------------------------- +*) + fun bool_commutative x y = + (x andalso y) = (y andalso x) + + fun number_commutative x y = + x * y = y * x + + fun list_reverse xs = + reverse(reverse xs) = xs + + fun int_gen_stays_in_interval i = + (integer(0, i) i).raw <= i + + fun abs_value_is_always_pos i = + abs_value i >= 0 + + fun my_floor_test i = + my_floor i = floor i + + fun my_length_test xs = + my_length xs = length xs + + fun make_list_test i = + let val generator = generator_gen i + fun f() = generator ((int_gen(0, inf) i).raw) + val ls = (make_list (f, i)) in + (length ls) = i end + + fun my_count_returns_non_negative_int x xs = + (my_count x xs) >= 0 + + fun rec_test rec i = + {theInteger = rec.theInteger, theString = rec.theString, z = i} = {rec with z = i} + + fun pre_pos x = + x >= 0 + + fun my_floor_test i = + my_floor i = floor i + + fun my_ceil_1_test i = + my_ceil_1 i = ceil i + + fun my_ceil_2_test i = + my_ceil_2 i = ceil i + + fun both_ceil_test i = + my_ceil_1 i = my_ceil_2 i + + fun tup_test x y z w = x+y+z+w < 100 (* = w+z+y+x *) + + fun no_args() = true + + fun test_bad_insert xs x = + length (bad_insert xs x) = (length xs) + 1 + + fun test_bad_half n = + n > (bad_half n) + + fun append_always_longer s1 s2 = + string_length s1 < string_length (s1 ^ s2) + + fun record_shrink_test r = + r.theInteger < 50 + +(* +-------------------------------- +USED FOR USERGUIDE - g +-------------------------------- +*) + fun filter_less ([], _) = [] + | filter_less ((x::xs), p) = + if x < p then append [x] (filter_less (xs, p)) else (filter_less (xs, p)) + + fun filter_greater ([], _) = [] + | filter_greater ((x::xs), p) = + if x > p then append [x] (filter_greater (xs, p)) else (filter_greater (xs, p)) + + + fun my_quicksort [] = [] + | my_quicksort (x::xs) = + let val smaller = my_quicksort(filter_less(xs, x)) + val greater = my_quicksort(filter_greater(xs, x)) in + append (append smaller [x]) (greater) end + + fun ordered [] = true + | ordered (x::[]) = true + | ordered (x::y::ys) = + if x <= y then ordered (y::ys) else false + + fun my_sort_is_ordered xs = + ordered (my_quicksort xs) + + fun my_sort_keep_length xs = + length xs = length (my_quicksort(xs)) + + fun pre_list_size_greater_than_one xs = + if (length xs) <= 1 then false else true + + fun no_duplicates[] = true + | no_duplicates (x::xs) = if (elem x xs) then false else no_duplicates xs + + fun cons_length_increase xs x = + (length (x::xs)) = ((length xs) + 1) +(* +-------------------------------- +TC^2 - z +-------------------------------- +*) + fun tc_sort_length_always_fails () = + for_all [list(integer())] my_sort_keep_length = false + + fun tc_sort_ordered_always_true () = + for_all [list(integer())] my_sort_is_ordered = true + +(* +-------------------------------- +CUSTOM TYPE PROGRAM +-------------------------------- +*) + fun eval exp env = + case exp of + ("num", n) => n + | ("var", n) => lookup env n ("unknown variable " ^ n) + | ("add", e1, e2) => (eval e1 env) + (eval e2 env) + | ("sub", e1, e2) => (eval e1 env) - (eval e2 env) + | ("mul", e1, e2) => (eval e1 env) * (eval e2 env) + | ("div", e1, e2) => (eval e1 env) / (eval e2 env) + | _ => print ("Error: ill defined expression"); exit (authority, 1) + + fun execute stmt env = + case stmt of + ("assign", var, exp) => + let val value = eval exp env + in + append [(var, value)] env + end + | ("print", exp) => (print (toString (eval exp env)); env) + + fun interpret prog = + let fun interpretHelper [] env = env + | interpretHelper (stmt :: rest) env = + let val newEnv = execute stmt env + in + interpretHelper rest newEnv + end + val (stmts, exp) = prog + val last_env = (interpretHelper stmts []) + in + eval exp last_env + end + + fun optimize_prog prog = + let val stmts = remove_nth ((length prog)-1) prog 0 + val exp = nth prog (length prog) + fun optimize_exp exp = + case exp of + ("num", n) => ("num", n) + | ("var", x) => ("var", x) + | ("add", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1+n2)) + |_ => ("add", (optimize_exp e1), (optimize_exp e2))) + | _ => ("add", (optimize_exp e1), (optimize_exp e2))) + | ("sub", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1-n2)) + |_ => ("sub", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("sub", (optimize_exp e1), (optimize_exp e2))) + | ("mul", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1*n2)) + |_ => ("mul", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("mul", (optimize_exp e1), (optimize_exp e2))) + | ("div", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => if ((n1 = 0) andalso (n2 = 0)) then ("div", e1, e2) else ("num", (n1/n2)) + |_ => ("div", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("div", (optimize_exp e1), (optimize_exp e2))) + + fun optimize_stmt stmt = + case stmt of + ("assign", var, exp) => ("assign", var, (optimize_exp exp)) + | ("print", exp) => ("print", (optimize_exp exp)) + in + append (map optimize_stmt stmts) [optimize_exp exp] + end + + fun exp_gen ls nesting_level size = + let val exp_ts = if length ls = 0 then ["num", "add", "sub", "mul", "div"] else ["num", "var", "add", "sub", "mul", "div"] + val exp_type = if nesting_level = 2 then "num" else one_of exp_ts + in + case exp_type of + "num" => + let val value = int_gen(inf, inf) size + fun shrinker inst = + let val shrunk_val = value.shrinker {state = inst.state, curr = inst.curr.1, prev = inst.prev.1} in + {state = shrunk_val.state, curr = ("num", shrunk_val.curr), prev = ("num", shrunk_val.prev)} end in + {raw = ("num", value.raw), shrinker = shrinker} end + | "var" => + let val value = one_of ls + fun shrinker inst = + {inst with state = "done"} in + {raw = ("var", value), shrinker = shrinker} end + |"add" => + let val e1 = exp_gen ls (nesting_level+1) size + val e2 = exp_gen ls (nesting_level+1) size + fun shrinker inst = + let val shrunk_e1 = e1.shrinker {state = inst.state, curr = inst.curr.1, prev = inst.prev.1} + val shrunk_e2 = e2.shrinker {state = inst.state, curr = inst.curr.2, prev = inst.prev.2} + val next_state = if shrunk_e1.state = "done" then shrunk_e2.state else shrunk_e1.state + in + {state = next_state, curr = ("add", shrunk_e1.curr, shrunk_e2.curr), prev = inst.prev} + end + in + {raw = ("add", e1.raw, e2.raw), shrinker = shrinker} + end + |"sub" => + let val e1 = exp_gen ls (nesting_level+1) size + val e2 = exp_gen ls (nesting_level+1) size + fun shrinker inst = + let val shrunk_e1 = e1.shrinker {state = inst.state, curr = inst.curr.1, prev = inst.prev.1} + val shrunk_e2 = e2.shrinker {state = inst.state, curr = inst.curr.2, prev = inst.prev.2} + val next_state = if shrunk_e1.state = "done" then shrunk_e2.state else shrunk_e1.state + in + {state = next_state, curr = ("sub", shrunk_e1.curr, shrunk_e2.curr), prev = inst.prev} + end + in + {raw = ("sub", e1.raw, e2.raw), shrinker = shrinker} + end + |"mul" => + let val e1 = exp_gen ls (nesting_level+1) size + val e2 = exp_gen ls (nesting_level+1) size + fun shrinker inst = + let val shrunk_e1 = e1.shrinker {state = inst.state, curr = inst.curr.1, prev = inst.prev.1} + val shrunk_e2 = e2.shrinker {state = inst.state, curr = inst.curr.2, prev = inst.prev.2} + val next_state = if shrunk_e1.state = "done" then shrunk_e2.state else shrunk_e1.state + in + {state = next_state, curr = ("mul", shrunk_e1.curr, shrunk_e2.curr), prev = inst.prev} + end + in + {raw = ("mul", e1.raw, e2.raw), shrinker = shrinker} + end + |"div" => + let val e1 = exp_gen ls (nesting_level+1) size + val e2 = exp_gen ls (nesting_level+1) size + fun shrinker inst = + let val shrunk_e1 = e1.shrinker {state = inst.state, curr = inst.curr.1, prev = inst.prev.1} + val shrunk_e2 = e2.shrinker {state = inst.state, curr = inst.curr.2, prev = inst.prev.2} + val next_state = if shrunk_e1.state = "done" then shrunk_e2.state else shrunk_e1.state + in + {state = next_state, curr = ("div", shrunk_e1.curr, shrunk_e2.curr), prev = inst.prev} + end + in + {raw = ("div", e1.raw, e2.raw), shrinker = shrinker} (* maybe just shrinker? *) + end + end + + fun assign_stmt_gen ls size = + let val n = string_gen size + val exp = exp_gen ls 0 size + fun shrinker inst = + let val shrunk_exp = exp.shrinker {state = inst.state, curr = inst.curr.2, prev = inst.prev.2} + val shrunk_assign = ("assign", n.raw, shrunk_exp.curr) + in + {state = shrunk_exp.state, curr = shrunk_assign, prev = inst.curr} + end + in + {raw = ("assign", n.raw, exp.raw), shrinker = shrinker} + end + + fun print_stmt_gen ls size = + let val exp = exp_gen ls 0 size + fun shrinker inst = + let val shrunk_exp = exp.shrinker {state = inst.state, curr = inst.curr.1, prev = inst.prev.1} + val shrunk_print = ("print", shrunk_exp.curr) + in + {state = shrunk_exp.state, curr = shrunk_print, prev = inst.curr} + end + in + {raw = ("print", exp.raw), shrinker = shrinker} + end + + fun stmt_gen ls size = + let val stmt = one_of ["assign", "print"] + in + case stmt of + "assign" => + let val res = assign_stmt_gen ls size in + {raw = res.raw, shrinker = res.shrinker} end + |"print" => + let val res = print_stmt_gen ls size in + {raw = res.raw, shrinker = res.shrinker} end + end + + fun assign_in_use_aux stmt_or_exp assign idx = + case stmt_or_exp.0 of + "print" => + assign_in_use_aux stmt_or_exp.1 assign idx + | "assign" => + assign_in_use_aux stmt_or_exp.2 assign idx + | "var" => if stmt_or_exp.1 = assign then true else false + | "num" => false + | _ => + if assign_in_use_aux stmt_or_exp.1 assign idx then + true + else + assign_in_use_aux stmt_or_exp.2 assign idx + + fun assign_in_use [] idxs assign idx bool = (bool, idxs) + | assign_in_use (x::xs) idxs assign idx bool = + let val res = assign_in_use_aux x assign idx + in + if res then assign_in_use xs (append [idx] idxs) assign (idx+1) true + else assign_in_use xs idxs assign (idx+1) bool + end + + fun program_gen size = + let val num_of_insts = (int_gen(0, size) size ).raw + fun prog_gen_aux env p s 0 = (p, s, env) + | prog_gen_aux env p s i = + let val stmt = stmt_gen env size + val newEnv = if stmt.raw.0 = "assign" then (append [stmt.raw.1] env) else env + in + prog_gen_aux newEnv (append p [stmt.raw]) (append s [stmt.shrinker]) (i-1) + end + val (prog_stmts, stmts_shrinkers, last_env) = prog_gen_aux [] [] [] num_of_insts + val last_exp = exp_gen last_env 0 size + val prog = (prog_stmts, last_exp.raw) + fun stmts_shrinker inst = + case inst.state of + "init" => + let + val shrunk = shrink_list stmts_shrinkers inst + in + shrunk + end + | "cont_size" => + let val next_elem = nth inst.curr (length inst.curr) + in + if next_elem.0 = "assign" then + if (assign_in_use inst.curr [] (next_elem.1) 0 false).0 then + {inst with idx = inst.idx-1} + else if (next_elem.0 = "var") orelse (next_elem.0 = "num") orelse (next_elem.0 = "add") orelse (next_elem.0 = "sub") orelse + (next_elem.0 = "mul") orelse (next_elem.0 = "div") then + {inst with idx = inst.idx-1} + + else + shrink_list stmts_shrinkers inst + else + shrink_list stmts_shrinkers inst + end + | _ => + shrink_list stmts_shrinkers inst + val stmts_val = {raw = prog_stmts, shrinker = stmts_shrinker} + in + {raw = prog, shrinker = shrink_sized_aggregate [stmts_val, last_exp] build_tuple} + end + + fun test_prog_opt prog = + (interpret prog) = (interpret (optimize_prog prog)) + fun test_prog_shrink prog = + (interpret prog) < 100 + fun record_shrink_test r = + r.theInteger < 50 + fun prop_program_shrink() = for_all ([program_gen], test_prog_shrink) + fun prop_record_shrink() = for_all ([(record ["theInteger", "theString"] [integer(), string()])], record_shrink_test) + + fun even_number_gen size = + let val {raw, shrinker} = integer() size + val raw_res = raw * 2 + fun this_shrinker inst = + let val interim = shrinker {inst with curr = (inst.curr / 2), prev = (inst.prev / 2)} + val res = {interim with curr = (interim.curr * 2), prev = (interim.prev * 2)} + in res + end + in {raw = raw_res, shrinker = this_shrinker} + end + + fun even_test i = + (i mod 2 = 0) andalso (i < 10) + fun even_stmt() = + for_all ([even_number_gen], even_test) + + fun test_shrinking stmt prop n = + let fun aux acc 0 = acc + | aux acc i = + let val (_, ctx) = troupecheck [stmt] + val _ = print i + val pre = () + val timing = (shrink ctx prop pre).1 + val newAcc = timing :: acc + in aux newAcc (i-1) + end + in + aux [] n + end + + (* -----------Tests the shrinking of a record with an integer and a string *) + fun record_shrink_test r = + r.theInteger < 50 + + + (* -----------Tests the shrinking of a two strings*) + fun append_always_longer s1 s2 = + let fun string_to_list s = + let fun aux "" acc = acc + | aux s acc = + let val x = substring (s, 0, 1) + val xs = substring (s, 1, 1/0) + in aux xs (append acc [x]) + end + in aux s [] + end + fun string_length s = + length (string_to_list s) + in string_length s1 < string_length (s1 ^ s2) + end + + (* -----------Tests the shrinking of a list of integers *) + fun filter_less ([], _) = [] + | filter_less ((x::xs), p) = + if x < p then append [x] (filter_less (xs, p)) else (filter_less (xs, p)) + + fun filter_greater ([], _) = [] + | filter_greater ((x::xs), p) = + if x > p then append [x] (filter_greater (xs, p)) else (filter_greater (xs, p)) + + + fun my_quicksort [] = [] + | my_quicksort (x::xs) = + let val smaller = my_quicksort(filter_less(xs, x)) + val greater = my_quicksort(filter_greater(xs, x)) in + append (append smaller [x]) (greater) end + fun my_sort_keep_length xs = + length xs = length (my_quicksort(xs)) + + (* -----------Tests the shrinking of a list of strings and a single string *) + fun bad_insert xs x = + if length xs < 10 then append [x] xs else + xs + fun test_bad_insert xs x = + length (bad_insert xs x) = (length xs) + 1 + + (* -----------Tests the shrinking of a float and a one_of statement with a long list *) + fun float_one_of_bad_shrink flt oneOf = + if (flt > 50) andalso (oneOf >= 1) then false else true + + + fun record_int_string_shrink() = for_all ([(record (["theInteger", "theString"], [integer(), string()]))], record_shrink_test) + fun two_strings_shrink() = for_all ([string(), string()], append_always_longer) + fun integer_list_shrink() = for_all ([list(integer())], my_sort_keep_length) + fun string_and_string_list_shrink() = for_all ([list(string()), string()], test_bad_insert) + fun float_and_one_of_shrink() = for_all ([float(), one_of [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]], float_one_of_bad_shrink) +in + +(* +-------------------------------- +ALL TESTS - x +-------------------------------- +*) + +print (test_shrinking float_and_one_of_shrink float_one_of_bad_shrink 100) +(* tc [program_gen] test_prog_opt *) + +(* shrinking tests - x *) +(* tc [list(integer()), integer()] test_bad_insert; +tc [integer()] (test_bad_half, (fn x => x >= 15)); +tc [string(), string()] (append_always_longer, lengths_not_same); +tc [record ["theInteger", "theString"] [integer(), string()]] record_shrink_test; *) + +(* tc^2 tests *) +(* tc [] tc_sort_ordered_always_true; *) + +(* User guide tests *) +(* tc [list(integer()), integer()] cons_length_increase; +tc [list(integer())] my_sort_is_ordered; +tc [list(integer())] my_sort_keep_length; +tc [list(integer())] (my_sort_keep_length, no_duplicates); *) + +(* General functionality tests *) +(* tc [(record ["theInteger", "theString"][integer(), string()]), integer()] rec_test; +tc [] no_args; +tc [integer(), integer(), integer(), integer()] tup_test; +write "\nTesting on bools commutative:"; +tc [boolean(), boolean()] bool_commutative; +write "\nTesting on numbers commutative:"; +tc [integer(), integer()] number_commutative; +write "\nTesting on list reverse:"; +tc [list(integer())] list_reverse; +write "\nTesting on int_gen interval:"; +tc [integer()] (int_gen_stays_in_interval, pre_pos); +write "\nTesting on abs_value:"; +tc [one_of_two (integer(), float())] abs_value_is_always_pos; +write "\nTesting on my_floor:"; +tc [float()] my_floor_test; +write "\nTesting that my_count always return non-negative result:"; +tc_n [integer(), list(integer())] my_count_returns_non_negative_int 1000; +write "\nTesting my_length:"; +tc [list(integer())] my_length_test; +write "\nTesting make_list:"; +tc [pos_integer()] make_list_test; +write "Testing on my_ceil_1:"; +tc [float()] my_ceil_1_test; +write "Testing on my_ceil_2:"; +tc [float()] my_ceil_2_test; +write "Testing on both ceil functions:"; +tc [float()] both_ceil_test *) +end \ No newline at end of file diff --git a/troupecheck/tc_archive/tc_int_shrink.trp b/troupecheck/tc_archive/tc_int_shrink.trp new file mode 100644 index 0000000..d038814 --- /dev/null +++ b/troupecheck/tc_archive/tc_int_shrink.trp @@ -0,0 +1,976 @@ +import lists +(* +-------------------------------- +PRINTING TO CONSOLE + +Simple functions for more convenient printing to console. + +-------------------------------- +*) +let val out = getStdout authority + fun write x = fwrite (out, x) + + fun args_toString args = + let fun aux_toString acc (x0::x1::xs) = aux_toString (acc ^ (toString x0) ^ ", ") (x1::xs) + | aux_toString acc (x::xs) = acc ^ (toString x) in + aux_toString "" args end +(* +-------------------------------- +ERROR HANDLING + +Handles the printing of appropriate error messages for errors that may occur in the use of TroupeCheck. + +-------------------------------- +*) + fun report_error error_reason = + write "\u001B[31m \nError: "; (* Changing the print color to red *) + let val err_string = case error_reason of + ("cant_generate", tries) => "Couldn't produce an instance that satisfies all strict constraints after " + ^ (toString tries) ^ " tries.\n" + | ("cant_satisfy", tries) => "No valid test could be generated after " ^ (toString tries) ^ " tries.\n" + | ("non_boolean_result", _) => "The property or precondition code returned a non-boolean result.\n" + | ("type_mismatch", _) => "The types' structure doesn't match the property.\n" + | ("illegal_gen_def", _ ) => "Generator is defined wrong - use tuple() or record() to combine generators.\n" + | ("record_mismatch", _) => "the number of names provided for record generation, does not match the number of types provided.\n" + | ("shrinking_looped", _) => "Shrinking looped.\n" + | ("non_string_type", _) => "An element of non-string type found when trying to convert list to string.\n" + in + write (err_string ^ "\u001B[0m"); (* Changing the color back *) + exit (authority, 0) end + + fun boolean_check x = + if (getType x)<>"boolean" then report_error ("non_boolean_result", 0) else () + + fun function_not_done_check p = + if (getType p)<>"function" then report_error ("type_mismatch", 0) else () +(* +-------------------------------- +UTILS + +Different utility functions that are used across the library. + +-------------------------------- +*) + fun remove_nth n [] i = [] + | remove_nth n (x::xs) i = + if n = i then xs + else x :: (remove_nth n xs (i + 1)) + + fun make_list (f, i) = + case i of + 0 => [] + | _ => append [f()] (make_list (f, i-1)) + + fun abs_value x = + if x < 0 then -x else x + +(* TODO: handle when arguments are passed to a property that does not take arguments *) + fun apply_args p l = + case l of + [] => boolean_check (p()); p() (* this case is only reached if there are no generators to begin with *) + | (x::xs) => + let val res = foldl (fn (x,y) => function_not_done_check y; y x) p l in + boolean_check res; + res + end + + fun string_to_list s = + let fun aux "" acc = acc + | aux s acc = + let val x = substring (s, 0, 1) + val xs = substring (s, 1, 1/0) in + aux xs (append acc [x]) end in + aux s [] end + + (* Combines a list of individual strings to a single string *) + fun list_to_string ls = + foldl (fn (x,y) => if getType x <> "string" then report_error ("non_string_type", 0) else y ^ x) "" ls + + fun string_length s = + length (string_to_list s) + + fun report_fail_reason rec noOfTests= + case rec.failReason of + "false_prop" => + write "\nFailure at input: "; + write (args_toString rec.ctx); + write ("\nAfter running: " ^ (toString (noOfTests - rec.remTests + 1)) ^ " test(s)\n") + + fun build_record names vals = + let fun aux r [] [] = r + | aux r (n::ns) (v::vs) = + aux (recordExtend(r, n, v)) ns vs in + aux {} names vals + end + + (* Hardcoded until a tuple from list function is implemented in Troupe - an issue has been raised on GH.*) + fun build_tuple ls = + case ls of + [] => (0) + |[x] => (x) + |[x1,x2] => (x1,x2) + |[x1,x2,x3] => (x1,x2,x3) + |[x1,x2,x3,x4] => (x1,x2,x3,x4) + |[x1,x2,x3,x4,x5] => (x1,x2,x3,x4,x5) + |[x1,x2,x3,x4,x5,x6] => (x1,x2,x3,x4,x5,x6) + |[x1,x2,x3,x4,x5,x6,x7] => (x1,x2,x3,x4,x5,x6,x7) + |[x1,x2,x3,x4,x5,x6,x7,x8] => (x1,x2,x3,x4,x5,x6,x7,x8) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9] => (x1,x2,x3,x4,x5,x6,x7,x8,x9) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10] => (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) + |_ => (2, 3, 4, 5) + + fun dec_nth list idx = + let fun dec_nth_aux [] acc i = acc + | dec_nth_aux (x::xs) acc i = + case i = idx of + true => + let val dec_val = if x-1 <= 0 then 0 else floor (x/2) in + dec_nth_aux xs (append acc [dec_val]) (i+1) end + | false => dec_nth_aux xs (append acc [x]) (i+1) + in + dec_nth_aux list [] 0 end + + fun dec_all seq = + let fun dec_all_aux [] i = [] + | dec_all_aux (x::xs) i = + if x = 0 then + dec_all_aux xs (i+1) + else + append [(fn () => (dec_nth seq i))] [fn () => dec_all_aux xs (i+1)] in + dec_all_aux seq 0 end + + fun seqs_of_seq sequence lengths = + let fun aux seq acc 0 = (acc, seq) + | aux (x::xs) acc n = + aux xs (append acc [x]) (n-1) in + (foldl (fn (x,(acc, s)) => + let val (curr_acc, curr_seq) = aux s [] x in + (append acc [curr_acc], curr_seq) end)([], sequence) lengths).0 end + + fun cutoff_at list idx = + let fun aux ls acc 0 = acc + | aux (x::xs) acc i = + aux xs (append acc [x]) (i-1) in + aux list [] idx end + + fun for_i body 0 = body() + | for_i body to = body(); for_i body (to-1) +(* +-------------------------------- +SHRINKING + +Works by first using random shrinking when a failing example has been found (shrink & random_shrink_aux). +Random shrinking means simply generating new test cases with gradually smaller size, to find a case smaller than the original one. This rarely produces a minmal result. +The smallest randomly shrunk instance is then further shrunk using integrated shrinking. (integrated_shrink & shrink_aux) +Integrated shrinking means keeping track of all random decision made during generation, and then re-generating with smaller "random" decisions. + +This part of the code also contains the functionality for recording all random decisions, and replaying these random decisions (produce_rng, rc_rng & rep_rng). +All of these functions are spawned and then requests or updates may be send to them, so that the correct RNG's are used at different points in the code. + +-------------------------------- +*) + fun produce_rng rng = + receive [hn ("REQUEST_RNG", senderid) => + let val _ = send (senderid, rng) + in produce_rng rng end, + + hn ("UPDATE_RNG", senderid, new_rng) => + let val _ = send(senderid, "done") in + produce_rng new_rng end] + + val rng_producer = spawn (fn() => produce_rng ()) + + + fun rec_rng ls = + receive [hn ("REQUEST_RND", senderid) => + let val rnd = floor (random()*1000000) + val _ = send (senderid, rnd) + in rec_rng (append ls [rnd]) + end, + hn ("REQUEST_SEQ", senderid) => + let val _ = send (senderid, ls) + in rec_rng [] + end] + + fun rep_rng ls = + receive [hn ("REQUEST_RND", senderid) => + case ls of + (x::xs) => + let val _ = send (senderid, x) + in rep_rng xs + end + | [] => + let val _ = send (senderid, 0) + in rep_rng ls + end, + hn ("REQUEST_LEFT", senderid) => + let val _ = send (senderid, ls) + in rep_rng [] + end, + hn ("UPDATE_LS", new_ls) => + rep_rng new_ls] + + fun shrink_aux seqs gens lengths prop pre size counter = + let val _ = send(rng_producer, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + in case seqs of + (x1::x2::x3::xs) => + let val seqs_of_curr = seqs_of_seq (x2()) lengths + val args_and_leftovers = mapi (fn (i, x) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = x size + val _ = send (pid, ("REQUEST_LEFT", self())) + val left_overs = receive [hn x => x] + in (arg, left_overs) + end) gens + + val (test_args, left_over_seqs) = foldl (fn (x, (raws, left_overs)) => (append raws [x.0], append left_overs [x.1])) ([],[]) args_and_leftovers + val ret_seqs = mapi (fn (i,x) => + if (length x) = 0 then (nth seqs_of_curr (i+1)) + else cutoff_at (nth seqs_of_curr (i+1)) ((nth lengths (i+1))-(length x))) left_over_seqs + val precond_is_met = if (pre <> ()) then (apply_args pre test_args) else true + in + case (apply_args prop test_args) orelse (precond_is_met = false) of + true => shrink_aux (x1::x3()) gens lengths prop pre size counter + | false => integrated_shrink ret_seqs gens prop pre size (counter+1) + end + | (x::xs) => + let val seqs_of_curr = seqs_of_seq (x()) lengths + val test_args = mapi (fn (i, y) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = y size + in arg end) gens + val precond_is_met = if (pre <> ()) then (apply_args pre test_args) else true + in + case (apply_args prop test_args) orelse (precond_is_met = false) orelse (size < 0) of + true => + let val res = mapi (fn (i, y) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = y (size+1) + in arg end) gens in + {shrunk_ctx = res, count = counter} end + | false => shrink_aux [x] gens lengths prop pre (size-1) counter + + end + end + + and integrated_shrink sequences gens prop pre size counter = + let val (seqs_comb, seq_lengths) = foldl (fn (x, (seq, lengths)) => ((append seq x), (append lengths [(length x)]))) ([], []) sequences + in + if foldl (fn (x,y) => (x = 0) andalso y) true seqs_comb then + shrink_aux [seqs_comb] gens seq_lengths prop pre size counter + else + let val decreased_seqs = dec_all seqs_comb + val dec_seqs_w_root = append [fn() => seqs_comb] decreased_seqs + val res = shrink_aux dec_seqs_w_root gens seq_lengths prop pre size (counter) + in + res end + end + + fun random_shrink_aux sequences generators prop pre success size counter = + if (counter = 1000) orelse (size = 0) then {count = success, size = size, sequences = sequences} else + let val _ = send(rng_producer, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val new_size = size-1 + val (shrunk_args, shrunk_sequences) = + foldl (fn (x, (arg_acc, seq_acc)) => + let val arg = x new_size + val _ = send (pid, ("REQUEST_SEQ", self())) + val seq = receive [hn x => x] + in (append arg_acc [arg], append seq_acc [seq]) + end) ([],[]) generators + val precond_is_met = if (pre <> ()) then (apply_args pre shrunk_args) else true + in + case (apply_args prop shrunk_args) orelse (precond_is_met = false) of + true => random_shrink_aux sequences generators prop pre success size (counter+1) + | false => + random_shrink_aux shrunk_sequences generators prop pre (success+1) new_size (0) + end + + fun shrink sequence generators prop pre size counter = + let val rng_recorder = spawn (fn() => rec_rng []) + val _ = send (rng_producer, ("UPDATE_RNG", self(), rng_recorder)) + val _ = receive [hn x => ()] + val res = random_shrink_aux sequence generators prop pre 0 size counter + val rng_replayer = spawn (fn() => rep_rng []) + val _ = send (rng_producer, ("UPDATE_RNG", self(), rng_replayer)) + val _ = receive [hn x => ()] + in + integrated_shrink (res.sequences) generators prop pre res.size (res.count) end +(* +-------------------------------- +GENERATORS + +Contains generators for Troupe's built-in types. All generators must return a single instance of the type they generate, +and take a 'size' argument as the very last argument. +This size will be given to all generators in the generation of test cases (and shrinking). +Generators that take more arguments, will need to have these passed along to them before passing the generator to the testing facilities +(convenience functions for this are supplied later). + +It is recommended that all user defined generators only make use of pre-defined generators or their matching convenience functions +for random decisions (i.e. a call to float_gen/float() or int_gen/integer()), instead of having to send and receive the correct messages to the RNG threads. +However, it can be done if the users wishes to and understands what is going on. + +-------------------------------- +*) + fun float_gen (low, high) size = + let val _ = send (rng_producer, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + + val _ = send (pid, ("REQUEST_RND", self())) + val x = receive [hn x => x] + + val _ = send (pid, ("REQUEST_RND", self())) + val bool_int = receive [hn x => x] + + val bool = bool_int < (1000000/2) + val float_of_x = x/1000000 + + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + + val res = + case (lInf, hInf) of + (true, true) => if bool then float_of_x * size else -float_of_x * size + | (true, false) => high - (float_of_x * size) + | (false, true) => low + (float_of_x * size) + | (false, false) => low + (float_of_x * (high-low)) + in res + end + + fun int_gen (low, high) size = + let val res = floor (float_gen (low, high+1) size) + in res + end + + fun bool_gen size = + let val rnd = int_gen (0,1) size + val res = if rnd = 0 then false + else true + in res + end + + fun list_gen (generator) size = + let val length = (int_gen (0, size) size) + val res = make_list ((fn () => generator size), length) + in res + end + + (* NOTE: Generates only letters (upper and lower case) and numbers. *) + fun char_gen size = + let val chars = + ["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", + "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", + "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", + "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", + "0", "1", "2", "3", "4", "5", "6", "7", "8", "9"] + val x = (int_gen (1, ((length chars)-1)) size) + in nth chars x + end + + (* NOTE: Generates only strings of letters (upper and lower case) and numbers. *) + fun string_gen size = + let val char_ls = list_gen (char_gen) size + val string = list_to_string char_ls + in string + end + + (* ts: list of generators - used to generate values for fields *) + (* NOTE: Hardcoded for tuple of up to 10 elements - see build_tuple in 'UTILS' *) + fun tuple_gen ts size = + let val ts_vals = map (fn x => x size) ts + in build_tuple ts_vals + end + + (* ns: list of strings - will be used as fieldnames *) + (* ts: list of generators - used to generate values for fields *) + fun rec_gen ns ts size = + if (length ns) <> (length ts) then + report_error ("record_mismatch", 0) + else + let val ts_vals = map (fn x => x size) ts + val res = build_record ns ts_vals + in res + end + + (* TODO: needs to be completed... *) + fun generator_gen size = + let val rnd = int_gen (1,7) size + val inf = 1/0 + val res = if rnd = 1 then ((fn i => int_gen (inf, inf) i)) else + if rnd = 2 then ((fn i => bool_gen i)) else + if rnd = 3 then ((fn i => float_gen (inf, inf) i)) else + if rnd = 4 then ((fn i => string_gen i)) else + if rnd = 5 then ((fn i => char_gen i)) else + if rnd = 6 then ((fn i => tuple_gen (make_list ((fn () => int_gen(inf, inf) i), i)) i)) else + ((fn i => list_gen (int_gen(inf, inf)) i)) in + res end + +(* +-------------------------------- +CORE FUNCTIONALITY + +Handles running the tests (core_forall), shrinking, preparing the recorder RNG and reporting the results to the user (tc). + +-------------------------------- +*) + fun core_forall (generators, prop, 0, size, pre, cap) = {failReason = (), ctx = (), ctx_seq = (), remTests = 0, size = size} + |core_forall (generators, prop, i, size, pre, cap) = + let val _ = send(rng_producer, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val (args, sequences) = foldl (fn (x, (arg_acc, seq_acc)) => + let val arg = x size + val _ = send (pid, ("REQUEST_SEQ", self())) + val seq = receive [hn x => x] + in (append arg_acc [arg], append seq_acc [seq]) + end) ([],[])generators + in + case pre of + () => + if (apply_args prop args) then (write "."; core_forall (generators, prop, i-1, size+1, pre, cap)) + else + let val _ = write "!" + in {failReason = "false_prop", ctx = args, ctx_seq = sequences, remTests = i, size = size} + end + | _ => + if (apply_args pre args) then + if (apply_args prop args) then (write "."; core_forall (generators, prop, i-1, size+1, pre, cap)) + else + let val _ = write "!" + in {failReason = "false_prop", ctx = args, ctx_seq = sequences, remTests = i, size = size} + end + else + let val _ = write "x" + in if (size = cap) andalso (i*5 = cap) then report_error ("cant_satisfy", size) + else if size = cap then {failReason = (), ctx = (), ctx_seq = (), remTests = i, size = size} + else core_forall (generators, prop, i, size+1, pre, cap) + end + end + + fun for_all (generators, p) = for_all (generators, p, 100) + | for_all (generators, p, noOfTests) = + let val (prop, pre) = + case p of + (x,y) => (x,y) + | x => (x, ()) + val rng_recorder = spawn (fn() => rec_rng []) + val _ = send (rng_producer, ("UPDATE_RNG", self(), rng_recorder)) + val _ = receive [hn x => ()] + val res = core_forall (generators, prop, noOfTests, 0, pre, (noOfTests*5)) in + case res.failReason of + () => write ("\u001B[1m \u001B[32m \nSuccess: \u001B[0mPassed all " ^ (toString noOfTests) ^ " test(s).\n"); true + |_ => + report_fail_reason res noOfTests; + write ("\u001B[1m\u001B[34mShrinking\u001B[0m:"); + let val shrink_res = shrink res.ctx_seq generators prop pre res.size 0 in + write "\nFailing test case was shrunk to:\n"; + write (args_toString shrink_res.shrunk_ctx); + write ("\nAfter " ^ (toString shrink_res.count) ^ " iterations.\n"); + false + end + end + + fun troupecheck props = + let val n = toString (length props) + fun troupecheck_aux [] i = exit (authority, 0) + | troupecheck_aux (x::xs) i = + let val _ = write ("\nRunning test " ^ (toString i) ^ " of " ^ n ^ ":\n") + val self_id = self() + val _ = spawn (fn () => let val res = x() in send(self_id, "done") end ) + val _ = receive [hn x => ()] + in troupecheck_aux xs (i+1) end + in troupecheck_aux props 1 + end + +(* +-------------------------------- +CONVENIENCE FUNCTIONS + +These are functions that make it easier for the user to make use of the different generators, and define their own generators. + +-------------------------------- +*) + val inf = 1 / 0 + fun integer() = int_gen(inf, inf) + | integer (h, l) = int_gen(h, l) + + fun pos_integer() = integer(0, inf) + + fun neg_integer() = integer(inf, -1) + + fun float() = float_gen(inf, inf) + | float(h, l) = float_gen(h, l) + + fun pos_float() = float(0, inf) + + fun neg_float() = float(inf, 0) + + fun boolean() = bool_gen + + fun list() = list_gen(generator_gen()) + |list(type) = list_gen(type) + + fun string() = string_gen + + fun char() = char_gen + + fun tuple ts = tuple_gen ts + + fun record ns ts = rec_gen ns ts + + fun one_of ls = + let val idx = (int_gen (1, (length ls)) ((length ls))) + in + (nth ls idx) + end +(* +-------------------------------- +FUNCTIONS FOR TESTING + +These functions exist only to define some test properties later, which are used in the development of TroupeCheck, to make sure it works as expected. + +-------------------------------- +*) + fun my_reverse xs = + xs + + fun my_floor i = + if i >=0 then i - (i mod 1) + else i - (i mod 1) - 1 + + fun my_length [] = 0 + | my_length (x::xs) = 1 + (my_length xs) + + fun my_count y [] = 0 + | my_count y (x::xs) = + let val z = + if y = x then 1 else 0 + in + z + my_count y xs end + + fun my_floor i = + if i >=0 then i - (i mod 1) + else i - (i mod 1) - 1 + + fun my_ceil_1 i = + if i > 0 then i + (1 - (i mod 1)) + else i + (1 - (i mod 1)) - 1 + + fun my_ceil_2 i = + if i > 0 then (my_floor i) + 1 + else if i = 0 then 0 + else (my_floor i) + 1 + + fun bad_insert xs x = + if length xs < 10 then append [x] xs else + xs + + fun one_of_two (x, y) size = + let val bool = (bool_gen size) in + if bool then x size + else y size end + + fun bad_half n = + if n > 10 then n else n/2 + + fun lengths_not_same s1 s2 = + (string_length s1) <> (string_length s2) + +(* +-------------------------------- +PROPERTY FUNCTIONS FOR TESTING + +See 'FUNCTIONS FOR TESTING'. + +-------------------------------- +*) + fun bool_commutative x y = + (x andalso y) = (y andalso x) + + fun number_commutative x y = + x * y <= 50 + + fun list_reverse xs = + reverse(reverse xs) = xs + + fun int_gen_stays_in_interval i = + (integer(0, i) i) <= i + + fun abs_value_is_always_pos i = + abs_value i >= 0 + + fun my_floor_test i = + my_floor i = floor i + + fun my_length_test xs = + my_length xs = length xs + + fun make_list_test i = + let val generator = generator_gen i + fun f() = generator (int_gen(0, inf) i) + val ls = (make_list (f, i)) in + (length ls) = i end + + fun my_count_returns_non_negative_int x xs = + (my_count x xs) >= 0 + + fun rec_test rec i = + {theInteger = rec.theInteger, theString = rec.theString, z = i} = {rec with z = i} + + fun pre_pos x = + x >= 0 + + fun my_floor_test i = + my_floor i = floor i + + fun my_ceil_1_test i = + my_ceil_1 i = ceil i + + fun my_ceil_2_test i = + my_ceil_2 i = ceil i + + fun both_ceil_test i = + my_ceil_1 i = my_ceil_2 i + + fun tup_test x y z w = x+y+z+w < 100 (* = w+z+y+x *) + + fun no_args() = true + + fun test_bad_insert xs x = + length (bad_insert xs x) = (length xs) + 1 + + fun test_bad_half n = + n > (bad_half n) + + fun append_always_longer s1 s2 = + string_length s1 < string_length (s1 ^ s2) + + fun record_shrink_test r = + r.theInteger < 50 + +(* +-------------------------------- +PROPERTIES FOR TESTING + +see 'FUNCTIONS FOR TESTING'. + +-------------------------------- + *) + fun prop_bad_insert() = for_all ([list(integer()), integer()], test_bad_insert) + fun prop_bad_half() = for_all ([integer()], (test_bad_half, (fn x => x >= 15))) + fun prop_record_shrink() = for_all ([record ["theInteger", "theString"] [integer(), string()]], record_shrink_test) + fun prop_not_satisfied() = for_all ([boolean(), boolean()], bool_commutative) + fun prop_count_non_negative() = for_all ([integer(), list(integer())], my_count_returns_non_negative_int, 1000) +(* +-------------------------------- +USED FOR USERGUIDE + +Functions used for demonstrating how to use TroupeCheck in the userguide. + +-------------------------------- +*) + fun filter_less ([], _) = [] + | filter_less ((x::xs), p) = + if x < p then append [x] (filter_less (xs, p)) else (filter_less (xs, p)) + + fun filter_greater ([], _) = [] + | filter_greater ((x::xs), p) = + if x > p then append [x] (filter_greater (xs, p)) else (filter_greater (xs, p)) + + + fun my_quicksort [] = [] + | my_quicksort (x::xs) = + let val smaller = my_quicksort(filter_less(xs, x)) + val greater = my_quicksort(filter_greater(xs, x)) in + append (append smaller [x]) (greater) end + + fun ordered [] = true + | ordered (x::[]) = true + | ordered (x::y::ys) = + if x <= y then ordered (y::ys) else false + + fun my_sort_is_ordered xs = + ordered (my_quicksort xs) + + fun my_sort_keep_length xs = + length xs = length (my_quicksort(xs)) + + fun pre_list_size_greater_than_one xs = + if (length xs) <= 1 then false else true + + fun no_duplicates[] = true + | no_duplicates (x::xs) = if (elem x xs) then false else no_duplicates xs + + fun cons_length_increase xs x = + (length (x::xs)) = ((length xs) + 1) + + fun list_no_duplicates (generator) size = + let val length = (integer(0, size) size) + fun no_dups_aux acc 0 = acc + | no_dups_aux acc i = + let val value = generator size + in if elem value acc + then no_dups_aux acc i + else no_dups_aux (value::acc) (i-1) + end + in no_dups_aux [] length + end + + fun is_ordered_prop() = for_all ([list(integer())], my_sort_is_ordered) + + fun keep_length_prop() = for_all ([list_no_duplicates(integer())], my_sort_keep_length) + + fun keep_length_fixed_prop() = for_all ([list(integer())], (my_sort_keep_length, no_duplicates)) + + fun length_increase_prop() = for_all ([list(integer()), integer()], cons_length_increase) + +(* +-------------------------------- +TC^2 + +Functions for testing TroupeCheck using TroupeCheck. + +-------------------------------- +*) + fun tc_sort_length_always_fails () = + for_all ([list(integer())], my_sort_keep_length) = false + + fun tc_sort_ordered_always_true () = + for_all ([list(integer())], my_sort_is_ordered) = true + +(* +-------------------------------- +CUSTOM TYPE PROGRAM + +Used for testing the creation of complex custom generators. +Here we defined an interpreter and generator for simple programs consisting of: +expr := ("num", number) |("var", string) |("add", expr, expr) |("sub", expr, expr) |("mul", expr, expr) |("div", expr, expr) +stmt := ("assign", string, expr) |("print", expr) +prog := [[stmt], expr] + +-------------------------------- +*) + fun eval exp env = + case exp of + ("num", n) => n + | ("var", n) => lookup env n ("unknown variable " ^ n) + | ("add", e1, e2) => (eval e1 env) + (eval e2 env) + | ("sub", e1, e2) => (eval e1 env) - (eval e2 env) + | ("mul", e1, e2) => (eval e1 env) * (eval e2 env) + | ("div", e1, e2) => (eval e1 env) / (eval e2 env) + | _ => print ("Error: ill defined expression"); exit (authority, 1) + + fun execute stmt env = + case stmt of + ("assign", var, exp) => + let val value = eval exp env + in + append [(var, value)] env + end + | ("print", exp) => (()(* print ("from prog: " ^ (toString (eval exp env)) *); env) + + fun interpret prog = + let fun interpretHelper [] env = env + | interpretHelper (stmt :: rest) env = + let val newEnv = execute stmt env + in + interpretHelper rest newEnv + end + val stmts = remove_nth ((length prog)-1) prog 0 + val exp = nth prog (length prog) + val last_env = (interpretHelper stmts []) + in + eval exp last_env + end + + fun optimize_prog prog = + let val stmts = remove_nth ((length prog)-1) prog 0 + val exp = nth prog (length prog) + fun optimize_exp exp = + case exp of + ("num", n) => ("num", n) + | ("var", x) => ("var", x) + | ("add", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1+n2)) + |_ => ("add", (optimize_exp e1), (optimize_exp e2))) + | _ => ("add", (optimize_exp e1), (optimize_exp e2))) + | ("sub", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1-n2)) + |_ => ("sub", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("sub", (optimize_exp e1), (optimize_exp e2))) + | ("mul", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1*n2)) + |_ => ("mul", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("mul", (optimize_exp e1), (optimize_exp e2))) + | ("div", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => if ((n1 = 0) andalso (n2 = 0)) then ("div", e1, e2) else ("num", (n1/n2)) + |_ => ("div", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("div", (optimize_exp e1), (optimize_exp e2))) + + fun optimize_stmt stmt = + case stmt of + ("assign", var, exp) => ("assign", var, (optimize_exp exp)) + | ("print", exp) => ("print", (optimize_exp exp)) + in + append (map optimize_stmt stmts) [optimize_exp exp] + end + + fun exp_gen ls nesting_level size = + let val exp_ts = + if nesting_level = 2 then ["num"] + else (if length ls = 0 then ["num", "add", "sub", "mul", "div"] + else ["var", "num", "add", "sub", "mul", "div"]) + val exp_type = one_of exp_ts + in + case exp_type of + "num" => + let val value = int_gen(1, inf) size in + ("num", value) end + | "var" => + let val value = one_of ls in + ("var", value) end + |"add" => + let val e1 = exp_gen ls (nesting_level+1) size + val e2 = exp_gen ls (nesting_level+1) size + in + ("add", e1, e2) + end + |"sub" => + let val e1 = exp_gen ls (nesting_level+1) size + val e2 = exp_gen ls (nesting_level+1) size + in + ("sub", e1, e2) + end + |"mul" => + let val e1 = exp_gen ls (nesting_level+1) size + val e2 = exp_gen ls (nesting_level+1) size + in + ("mul", e1, e2) + end + |"div" => + let val e1 = exp_gen ls (nesting_level+1) size + val e2 = exp_gen ls (nesting_level+1) size + in + ("div", e1, e2) + end + end + + fun assign_stmt_gen ls size = + let val n = string_gen size + val exp = exp_gen ls 0 size + in + ("assign", n, exp) + end + + fun print_stmt_gen ls size = + let val exp = exp_gen ls 0 size + in + ("print", exp) + end + + fun stmt_gen ls size = + let val stmt = one_of ["print", "assign"] + in + case stmt of + "assign" => + let val res = assign_stmt_gen ls size in + res end + |"print" => + let val res = print_stmt_gen ls size in + res end + end + + fun program_gen size = + let val num_of_insts = (int_gen(0, size) size) + fun prog_gen_aux env p 0 = (p, env) + | prog_gen_aux env p i = + let val stmt = stmt_gen env size + val newEnv = if stmt.0 = "assign" then (append [stmt.1] env) else env + in + prog_gen_aux newEnv (append p [stmt]) (i-1) + end + val (prog_stmts, last_env) = prog_gen_aux [] [] num_of_insts + val last_exp = exp_gen last_env 0 size + val prog = append prog_stmts [last_exp] + in + prog + end + + fun test_prog_opt prog = + (interpret prog) = (interpret (optimize_prog prog)) + fun test_prog_shrink prog = + (interpret prog) < 100 + fun prop_program_shrink() = for_all ([program_gen], test_prog_shrink) + + +in + +troupecheck [keep_length_prop] + +(* for_all [list(integer()), integer()] test_bad_insert; +for_all [integer()] (test_bad_half, (fn x => x >= 15)); +for_all [string(), string()] (append_always_longer, lengths_not_same); +for_all [record ["theInteger", "theString"] [integer(), string()]] record_shrink_test; +for_all [program_gen] test_prog_opt; *) + +(* for_i (fn() => for_all [program_gen] test_prog_shrink) 50 *) +(* for_all [program_gen] test_prog_shrink *) + +(* +-------------------------------- +ALL TESTS - x +-------------------------------- +*) +(* for_all [integer(), integer()] number_commutative *) +(* shrinking tests - x *) +(* for_all [list(integer()), integer()] test_bad_insert; +for_all [integer()] (test_bad_half, (fn x => x >= 15)); +for_all [string(), string()] (append_always_longer, lengths_not_same); +for_all [record ["theInteger", "theString"] [integer(), string()]] record_shrink_test; *) + +(* tc^2 tests *) +(* for_all [] tc_sort_ordered_always_true; *) + +(* User guide tests *) +(* for_all [list(integer()), integer()] cons_length_increase; +for_all [list(integer())] my_sort_is_ordered; +for_all [list(integer())] my_sort_keep_length; +for_all [list(integer())] (my_sort_keep_length, no_duplicates) *) + +(* General functionality tests *) +(* for_all [(record ["theInteger", "theString"][integer(), string()]), integer()] rec_test; +for_all [] no_args; +for_all [integer(), integer(), integer(), integer()] tup_test; +write "\nTesting on bools commutative:"; +for_all [boolean(), boolean()] bool_commutative; +write "\nTesting on numbers commutative:"; +for_all [integer(), integer()] number_commutative; +write "\nTesting on list reverse:"; +for_all [list(integer())] list_reverse; +write "\nTesting on int_gen interval:"; +for_all [integer()] (int_gen_stays_in_interval, pre_pos); +write "\nTesting on abs_value:"; +for_all [one_of_two (integer(), float())] abs_value_is_always_pos; +write "\nTesting on my_floor:"; +for_all [float()] my_floor_test; +write "\nTesting that my_count always return non-negative result:"; +tc_n [integer(), list(integer())] my_count_returns_non_negative_int 1000; +write "\nTesting my_length:"; +for_all [list(integer())] my_length_test; +write "\nTesting make_list:"; +for_all [pos_integer()] make_list_test; +write "Testing on my_ceil_1:"; +for_all [float()] my_ceil_1_test; +write "Testing on my_ceil_2:"; +for_all [float()] my_ceil_2_test; +write "Testing on both ceil functions:"; +for_all [float()] both_ceil_test *) +end \ No newline at end of file diff --git a/troupecheck/tc_tests/calculator.trp b/troupecheck/tc_tests/calculator.trp new file mode 100644 index 0000000..055e7ff --- /dev/null +++ b/troupecheck/tc_tests/calculator.trp @@ -0,0 +1,43 @@ +import troupecheck +let fun calc expr = + case expr of + ("a", x, y) => + let val cx = (calc x) + val cy = (calc y) + in + if (cx = "nothing") orelse (cy = "nothing") then "nothing" else cx + cy + end + | ("d", x, y) => + (case calc y of + 0 => "nothing" + | r => + let val cx = (calc x) + in if (cx = "nothing") orelse (r = "nothing") then "nothing" else cx / r end) + | n => n + + fun divSubTerms expr = + case expr of + ("d", _, 0) => false + | (_, x, y) => (divSubTerms x) andalso (divSubTerms y) + | _ => true + + fun expr_gen tco tco 0 = integer() tco 0 + | expr_gen tco size = + let val res = + one_of [(integer() tco (size)), ("a", (expr_gen tco (size-1)), (expr_gen tco (size-1))), + ("d", (expr_gen tco (size-1)), (expr_gen tco (size-1)))] tco size + in + res + end + + fun expr() = expr_gen 4 + + fun prop_calculator() = + for_all([expr()], ((fn x => (getType (calc x)) <> "string"), divSubTerms)) +in troupecheck[prop_calculator] authority +end + + + + + diff --git a/troupecheck/tc_tests/general-testing.trp b/troupecheck/tc_tests/general-testing.trp new file mode 100644 index 0000000..b3d8ddf --- /dev/null +++ b/troupecheck/tc_tests/general-testing.trp @@ -0,0 +1,175 @@ +import lists +import troupecheck +(* +-------------------------------- +FUNCTIONS FOR TESTING + +These functions exist only to define some test properties later, which are used in the development of TroupeCheck, to make sure it works as expected. + +-------------------------------- +*) +let fun my_reverse xs = + xs + + fun abs_value x = + if x < 0 then -x else x + + fun my_floor i = + if i >=0 then i - (i mod 1) + else i - (i mod 1) - 1 + + fun my_length [] = 0 + | my_length (x::xs) = 1 + (my_length xs) + + fun my_count y [] = 0 + | my_count y (x::xs) = + let val z = + if y = x then 1 else 0 + in + z + my_count y xs end + + fun my_floor i = + if i >=0 then i - (i mod 1) + else i - (i mod 1) - 1 + + fun my_ceil1 i = + if i > 0 then i + (1 - (i mod 1)) + else i + (1 - (i mod 1)) - 1 + + fun my_ceil2 i = + if i > 0 then (my_floor i) + 1 + else if i = 0 then 0 + else (my_floor i) + 1 + + fun bad_insert xs x = + if length xs < 10 then append [x] xs else + xs + + fun one_of_two (x, y) tco size = + let val bool = (boolean() tco size) in + if bool then x tco size + else y tco size end + + fun bad_half n = + if n > 10 then n else n/2 + + fun string_to_list s = + let fun aux "" acc = acc + | aux s acc = + let val x = substring (s, 0, 1) + val xs = substring (s, 1, 1/0) in + aux xs (append acc [x]) end in + aux s [] end + + fun string_length s = + length (string_to_list s) + + fun lengths_not_same s1 s2 = + (string_length s1) <> (string_length s2) + + + +(* +-------------------------------- +PROPERTY FUNCTIONS FOR TESTING + +See 'FUNCTIONS FOR TESTING'. + +-------------------------------- +*) + fun bool_commutative x y = + (x andalso y) = (y andalso x) + + fun number_commutative x y = + x * y <= 50 + + fun list_reverse xs = + reverse(reverse xs) = xs + + fun int_gen_stays_in_interval i = + i <= 50 + + fun abs_value_is_always_pos i = + abs_value i >= 0 + + fun my_floor_test i = + my_floor i = floor i + + fun my_length_test xs = + my_length xs = length xs + +(* fun make_list_test generator i = + let fun dummy_tco_func() = receive [hn ("REQUEST_RND",sender) => let val _ = send (sender, random()) in dummy_tco_func end] + fun f() = generator (spawn (fn() => dummy_tco_func())) i + val ls = (make_list (f, i)) in + (length ls) = i end *) + + fun my_count_returns_non_negative_int x xs = + (my_count x xs) >= 0 + + fun rec_test rec i = + {theInteger = rec.theInteger, theString = rec.theString, z = i} = {rec with z = i} + + fun pre_pos x = + x >= 0 + + fun my_floor_test i = + my_floor i = floor i + + fun my_ceil1_test i = + my_ceil1 i = ceil i + + fun my_ceil2_test i = + my_ceil2 i = ceil i + + fun both_ceil_test i = + my_ceil1 i = my_ceil2 i + + fun shrink_test x y z w = x+y+z+w < 100 + + fun no_args() = true + + fun test_bad_insert xs x = + length (bad_insert xs x) = (length xs) + 1 + + fun test_bad_half n = + n > (bad_half n) + + fun append_always_longer s1 s2 = + string_length s1 < string_length (s1 ^ s2) + + fun record_shrink_test r = + r.theInteger < 50 + +(* +-------------------------------- +PROPERTIES FOR TESTING + +see 'FUNCTIONS FOR TESTING'. + +-------------------------------- + *) + fun prop_bad_insert() = for_all ([list(integer()), integer()], test_bad_insert) + fun prop_bad_half() = for_all_noshrink ([integer()], (test_bad_half, (fn x => x >= 15))) + fun prop_record_shrink() = for_all ([(record (["theInteger", "theString"], [integer(), string()]))], record_shrink_test) + fun prop_bool_commutative() = for_all ([boolean(), boolean()], bool_commutative) + fun prop_count_non_negative() = for_all ([integer(), list(integer())], my_count_returns_non_negative_int) (* 1000 *) + fun prop_rec_test() = for_all ([(record (["theInteger", "theString"], [integer(), string()])), integer()], rec_test) + fun prop_no_args() = for_all ([], no_args) + fun prop_shrink_test() = for_all ([integer(), integer(), integer(), integer()], shrink_test) + fun prop_number_commutative() = for_all ([integer(), integer()], number_commutative) + fun prop_list_reverse() = for_all ([list(integer())], list_reverse) + fun prop_integer_interval_works() = for_all ([integer(0, 50)], (int_gen_stays_in_interval, pre_pos)) + fun prop_abs_value() = for_all ([(one_of_two (integer(), float()))], abs_value_is_always_pos) + fun prop_floor() = for_all ([float()], my_floor_test) + fun prop_my_length() = for_all ([list(integer())], my_length_test) + (* fun prop_make_list_test() = for_all ([generator(), integer(0, 10)], make_list_test) *) (* Doesn't work... *) + fun prop_my_ceil1() = for_all ([float()], my_ceil1_test) + fun prop_my_ceil2() = for_all ([float()], my_ceil2_test) + fun prop_both_ceil() = for_all ([float()], both_ceil_test) + + val test_list = [prop_bad_insert, prop_bad_half, prop_record_shrink, prop_bool_commutative, prop_count_non_negative, prop_rec_test, + prop_no_args, prop_shrink_test, prop_number_commutative, prop_list_reverse, prop_integer_interval_works, prop_abs_value, + prop_floor, prop_my_length, prop_my_ceil1, prop_my_ceil2, prop_both_ceil] +in troupecheck test_list authority +end \ No newline at end of file diff --git a/troupecheck/tc_tests/shrinking-tests.trp b/troupecheck/tc_tests/shrinking-tests.trp new file mode 100644 index 0000000..e37025d --- /dev/null +++ b/troupecheck/tc_tests/shrinking-tests.trp @@ -0,0 +1,136 @@ +(* + This file is purely for testing different aspects of how well TroupeCheck handles shrinking. + If any changes are made to the shrinking part of the TC library, it is a good idea to run all of these, and + check that the shrinks look as one would expect. + They can be run with the command 'make tc-shrink-tests' from the troupecheck folder. +*) +import troupecheck +import lists +(* +-------------------------------- +UTILITY FUNCTIONS FOR +BOOLEAN STATEMENTS. + +-------------------------------- +*) +let fun filter_less ([], _) = [] + | filter_less ((x::xs), p) = + if x < p then append [x] (filter_less (xs, p)) else (filter_less (xs, p)) + + fun filter_greater ([], _) = [] + | filter_greater ((x::xs), p) = + if x > p then append [x] (filter_greater (xs, p)) else (filter_greater (xs, p)) + + + fun my_quicksort [] = [] + | my_quicksort (x::xs) = + let val smaller = my_quicksort(filter_less(xs, x)) + val greater = my_quicksort(filter_greater(xs, x)) in + append (append smaller [x]) (greater) end + + fun filter_less2 ([], _) = [] + | filter_less2 ((x::xs), p) = + if ((x <= p) andalso (x<>0)) orelse (p = 0) then append [x] (filter_less2 (xs, p)) else (filter_less2 (xs, p)) + + fun filter_greater2 ([], _) = [] + | filter_greater2 ((x::xs), p) = + if ((x > p) andalso (p<>0)) orelse (x = 0) then append [x] (filter_greater2 (xs, p)) else (filter_greater2 (xs, p)) + + fun my_quicksort2 [] = [] + | my_quicksort2 (x::xs) = + let val smaller = my_quicksort2(filter_less2(xs, x)) + val greater = my_quicksort2(filter_greater2(xs, x)) in + append (append smaller [x]) (greater) end + + fun filter_less3 ([], _) = [] + | filter_less3((x::xs), p) = + if (x < p)andalso (x<>15) then append [x] (filter_less3 (xs, p)) else (filter_less3 (xs, p)) + + fun filter_greater3 ([], _) = [] + | filter_greater3 ((x::xs), p) = + if (x >= p) andalso (x<>15) then append [x] (filter_greater3 (xs, p)) else (filter_greater3 (xs, p)) + + fun my_quicksort3 [] = [] + | my_quicksort3 (x::xs) = + let val smaller = my_quicksort3(filter_less3(xs, x)) + val greater = my_quicksort3(filter_greater3(xs, x)) in + append (append smaller [x]) (greater) end + + + + + + fun bad_insert xs x = + if length xs < 10 then append [x] xs else + xs + + fun bad_half n = + if n > 10 then n else n/2 + + fun ordered [] = true + | ordered (x::[]) = true + | ordered (x::y::ys) = + if x <= y then ordered (y::ys) else false +(* +-------------------------------- +BOOLEAN STATEMENTS FOR TESTING. + +-------------------------------- +*) + fun shrink_test x y z w = x+y+z+w < 100 + + fun test_bad_insert xs x = + length (bad_insert xs x) = (length xs) + 1 + + fun test_bad_half n = + n > (bad_half n) + + fun record_shrink_test r = + r.theInteger < 50 + + fun append_always_longer s1 s2 = + let fun string_to_list s = + let fun aux "" acc = acc + | aux s acc = + let val x = substring (s, 0, 1) + val xs = substring (s, 1, 1/0) + in aux xs (append acc [x]) + end + in aux s [] + end + fun string_length s = + length (string_to_list s) + in string_length s1 < string_length (s1 ^ s2) + end + + fun my_sort_keep_length xs = + length xs = length (my_quicksort(xs)) + + fun mysort2_is_ordered xs = + ordered (my_quicksort2 xs) + + fun mysort3_keep_length xs = + length xs = length (my_quicksort3(xs)) + + fun tuple_shrink_test (number, string) = + number < 50 + +(* +-------------------------------- +PROPERTIES TO RUN WITH TROUPECHECK. + +-------------------------------- +*) + fun prop_append_always_longer() = for_all ([string(), string()], append_always_longer) + fun prop_bad_insert() = for_all ([list(integer()), integer()], test_bad_insert) + fun prop_bad_half() = for_all ([integer()], (test_bad_half, (fn x => x >= 15))) + fun prop_record_shrink() = for_all ([(record (["theInteger", "theString"], [integer(), string()]))], record_shrink_test) + fun prop_shrink_test() = for_all ([integer(), integer(), integer(), integer()], shrink_test) + fun prop_keep_length() = for_all ([list(integer())], my_sort_keep_length) + fun prop_mysort2_ordered() = for_all ([list(integer())], mysort2_is_ordered) + fun prop_mysort3_keep_length() = for_all ([list(integer())], mysort3_keep_length) + fun prop_tuple_shrink() = for_all ([tuple([integer(), string()])], tuple_shrink_test) + val prop_list = [prop_append_always_longer, prop_bad_insert, prop_bad_half, prop_record_shrink, + prop_shrink_test, prop_keep_length, prop_mysort2_ordered, prop_mysort3_keep_length, prop_tuple_shrink] +in troupecheck prop_list authority +end \ No newline at end of file diff --git a/troupecheck/tc_tests/userguide-tests.trp b/troupecheck/tc_tests/userguide-tests.trp new file mode 100644 index 0000000..829ddf7 --- /dev/null +++ b/troupecheck/tc_tests/userguide-tests.trp @@ -0,0 +1,67 @@ +import lists +import troupecheck +(* +-------------------------------- +USED FOR USERGUIDE + +Functions used for demonstrating how to use TroupeCheck in the userguide. + +-------------------------------- +*) +let fun filter_less ([], _) = [] + | filter_less ((x::xs), p) = + if x < p then append [x] (filter_less (xs, p)) else (filter_less (xs, p)) + + fun filter_greater ([], _) = [] + | filter_greater ((x::xs), p) = + if x > p then append [x] (filter_greater (xs, p)) else (filter_greater (xs, p)) + + + fun my_quicksort [] = [] + | my_quicksort (x::xs) = + let val smaller = my_quicksort(filter_less(xs, x)) + val greater = my_quicksort(filter_greater(xs, x)) in + append (append smaller [x]) (greater) end + + fun ordered [] = true + | ordered (x::[]) = true + | ordered (x::y::ys) = + if x <= y then ordered (y::ys) else false + + fun my_sort_is_ordered xs = + ordered (my_quicksort xs) + + fun my_sort_keep_length xs = + length xs = length (my_quicksort(xs)) + + fun pre_list_size_greater_than_one xs = + if (length xs) <= 1 then false else true + + fun no_duplicates[] = true + | no_duplicates (x::xs) = if (elem x xs) then false else no_duplicates xs + + fun cons_length_increase xs x = + (length (x::xs)) = ((length xs) + 1) + + fun list_no_duplicates (generator) tco size = + let val length = (integer(0, size) tco size) + fun no_dups_aux acc 0 = acc + | no_dups_aux acc i = + let val value = generator tco size + in if elem value acc + then no_dups_aux acc i + else no_dups_aux (value::acc) (i-1) + end + in no_dups_aux [] length + end + + fun is_ordered_prop() = for_all ([list(integer())], my_sort_is_ordered) + + fun keep_length_prop() = for_all ([list(integer())], my_sort_keep_length) + + fun keep_length_fixed_prop() = for_all ([list(integer())], (my_sort_keep_length, no_duplicates)) + + fun length_increase_prop() = for_all ([list(integer()), integer()], cons_length_increase) +in +troupecheck [keep_length_prop, length_increase_prop] authority +end diff --git a/troupecheck/timing-experiments/booltest.trp b/troupecheck/timing-experiments/booltest.trp new file mode 100644 index 0000000..9a91b39 --- /dev/null +++ b/troupecheck/timing-experiments/booltest.trp @@ -0,0 +1,35 @@ +import troupecheck +import lists +(* NOTE: In order run this the 'troupecheck.trp' library file must be modified, + so that the troupecheck function does not exit the runtime - i.e. replace the call to 'exit(authority, 0)' + with '()', and run make libs, from Troupe directory. + Remember to change back! *) +(* This file times how long it takes takes troupecheck to test a property on tuples, that is always true. + It times this process 100 times and returns the average *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun bool_commutative x y = + (x andalso y) = (y andalso x) + + fun prop_bool_test() = for_all ([boolean(), boolean()], bool_commutative) + + fun test_troupecheck(ls, 0) = ls + | test_troupecheck(ls, n) = + let val startT = getTime() + val _ = troupecheck [prop_bool_test] authority + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newList = append ls [elapsedMilliseconds] + val newN = (n-1) + in test_troupecheck(newList, newN) + end +in average (test_troupecheck([], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/constest.trp b/troupecheck/timing-experiments/constest.trp new file mode 100644 index 0000000..41d6f5b --- /dev/null +++ b/troupecheck/timing-experiments/constest.trp @@ -0,0 +1,24 @@ +import lists +(* This file times how long it takes takes troupe to cons an element in front of a list. *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun test_cons(ls, timings, 0) = timings + | test_cons(ls, timings, n) = + let val startT = getTime() + val newList = n :: ls + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newTimings = append timings [elapsedMilliseconds] + val newN = (n-1) + in test_cons(newList, newTimings, newN) + end +in average (test_cons([], [], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/floattest.trp b/troupecheck/timing-experiments/floattest.trp new file mode 100644 index 0000000..c131c98 --- /dev/null +++ b/troupecheck/timing-experiments/floattest.trp @@ -0,0 +1,45 @@ +import lists +(* This file times how long it takes takes troupe to cons an element in front of a list. *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun float_gen (low, high) tco size = + let val x = random() + + val bool_int = random () + + val bool = bool_int < (1/2) + + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + + val res = + case (lInf, hInf) of + (true, true) => if bool then x * size else -x * size + | (true, false) => high - (x * size) + | (false, true) => low + (x * size) + | (false, false) => low + (x * (high-low)) + in res + end + + val inf = 1/0 + + fun test_float(timings, 0) = timings + | test_float(timings, n) = + let val startT = getTime() + val _ = float_gen(inf, inf) () n + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newTimings = append timings [elapsedMilliseconds] + val newN = (n-1) + in test_float(newTimings, newN) + end +in average (test_float([], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/floortest.trp b/troupecheck/timing-experiments/floortest.trp new file mode 100644 index 0000000..b50844d --- /dev/null +++ b/troupecheck/timing-experiments/floortest.trp @@ -0,0 +1,51 @@ +import lists +(* This file times how long it takes takes troupe to cons an element in front of a list. *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun float_gen (low, high) tco size = + let val x = random() + + val bool_int = random () + + val bool = bool_int < (1/2) + + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + + val res = + case (lInf, hInf) of + (true, true) => if bool then x * size else -x * size + | (true, false) => high - (x * size) + | (false, true) => low + (x * size) + | (false, false) => low + (x * (high-low)) + in res + end + + fun int_gen (low, high) tco size = + let val res = floor (float_gen (low, high+1) tco size) + in res + end + + val inf = 1/0 + + fun test_floor(timings, 0) = timings + | test_floor(timings, n) = + let val float = float_gen(inf, inf) () n + val startT = getTime() + val _ = floor float + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newTimings = append timings [elapsedMilliseconds] + val newN = (n-1) + in test_floor(newTimings, newN) + end +in average (test_floor([], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/gen-and-apply-timings.trp b/troupecheck/timing-experiments/gen-and-apply-timings.trp new file mode 100644 index 0000000..c1d7a2f --- /dev/null +++ b/troupecheck/timing-experiments/gen-and-apply-timings.trp @@ -0,0 +1,170 @@ +import lists +import troupecheck +(* This file is for testing what causes TroupeChecks slow overhead, + by timing the apply args function, and the foldl call that generates the arguments. *) +let fun bool_commutative x y = + (x andalso y) = (y andalso x) + val bool_test_gens = [boolean(), boolean()] + + fun tuple_test (number, string) = + getType number = "number" + + val tup_test_gens = [tuple([integer(), string()])] + + val gens_to_use = bool_test_gens + val test_to_use = bool_commutative + fun init_tc auth rng = + receive [hn ("REQUEST_RNG", senderid) => + let val _ = send (senderid, rng) + in init_tc auth rng end, + + hn ("REQUEST_AUTH", senderid) => + let val _ = send (senderid, auth) + in init_tc auth rng end, + + hn ("UPDATE_RNG", senderid, new_rng) => + let val _ = send(senderid, "done") in + init_tc auth new_rng end] + + fun rec_rng ls = + receive [hn ("REQUEST_RND", senderid) => + let val rnd = random() + val _ = send (senderid, rnd) + in rec_rng (rnd :: ls) + end, + hn ("REQUEST_SEQ", senderid) => + let val _ = send (senderid, (reverse ls)) + in rec_rng [] + end] + val recorder = spawn(fn() => rec_rng []) + val tcp = spawn(fn() => init_tc authority recorder) + + fun boolean_check x tco = + if (getType x)<>"boolean" then () else () + + fun function_not_done_check p tco = + if (getType p)<>"function" then () else () + + fun apply_args p l tco = + let val _ = send (tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + in case l of + [] => (* this case is only reached if there are no generators to begin with *) + let val _ = boolean_check (p()) tco + val res = p() + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + | (x::xs) => + let val res = foldl (fn (x,y) => function_not_done_check y tco; y x) p l + val _ = boolean_check res tco + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + end + + fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun handle_inner_timings timings = + let val (arg, rec, ap_ac, ap_seq) = timings + val arg_avrg = average arg + val rec_avrg = average rec + val ap_ac_avrg = average ap_ac + val ap_seq_avrg = average ap_seq + in (arg_avrg, rec_avrg, ap_ac_avrg, ap_seq_avrg) + end + + fun append_inner_timings to_append to = + let val (a1, b1, c1, d1) = to + val (a2, b2, c2, d2) = to_append + val a3 = append a1 [a2] + val b3 = append b1 [b2] + val c3 = append c1 [c2] + val d3 = append d1 [d2] + in (a3, b3, c3, d3) + end + + fun sum_inner_timings timings = + let val (a1, b1, c1, d1) = timings + val a2 = sum a1 + val b2 = sum b1 + val c2 = sum c1 + val d2 = sum d1 + in (a2, b2, c2, d2) + end + + fun test_troupecheck_inner(gen_ts, app_ts, inner_timings, 101) = (gen_ts, app_ts, inner_timings) + | test_troupecheck_inner (gen_ts, app_ts, inner_timings, n) = + let val generators = gens_to_use + val start_gen = getTime() + val (args, sequences, times) = foldl (fn (x, (arg_acc, seq_acc, (arg_t, rec_t, ap_ac_t, ap_seq_t))) => + let val arg_start = getTime() + val arg = x tcp n + val arg_end = getTime() + val _ = send (recorder, ("REQUEST_SEQ", self())) + val rec_start = getTime() + val seq = receive [hn x => x] + val rec_end = getTime() + val ap_ac_start = getTime() + val new_args = append arg_acc [arg] + val ap_ac_end = getTime() + val ap_seq_start = getTime() + val new_seqs = append seq_acc [seq] + val ap_seq_end = getTime() + val new_arg_t = append arg_t [arg_end - arg_start] + val new_rec_t = append rec_t [rec_end - rec_start] + val new_ap_ac_t = append ap_ac_t [ap_ac_end - ap_ac_start] + val new_ap_seq_t = append ap_seq_t [ap_seq_end - ap_seq_start] + in (new_args, new_seqs, (new_arg_t, new_rec_t, new_ap_ac_t, new_ap_seq_t)) + end) ([],[], ([], [], [], [])) generators + val end_gen = getTime() + val inner_timings_avrg = handle_inner_timings times + val new_inner_timings = append_inner_timings inner_timings_avrg inner_timings + val start_app = getTime() + val _ = apply_args test_to_use args tcp + val end_app = getTime() + in test_troupecheck_inner(append gen_ts [end_gen-start_gen], append app_ts [end_app - start_app], new_inner_timings, (n+1)) + end + + fun print_inners inners = + let val (a1, b1, c1, d1) = inners + val _ = print "arg generation:" + val _ = print a1 + val _ = print "recive seq:" + val _ = print b1 + val _ = print "append arg:" + val _ = print c1 + val _ = print "append sequence:" + val _ = print d1 + in () + end + + fun test_troupecheck(ls1,ls2, inners, 0) = (ls1,ls2, inners) + | test_troupecheck(ls1,ls2, inners, n) = + let val (gens, apps, timings) = test_troupecheck_inner([], [], ([], [], [], []), 0) + val gen_sum = sum gens 0 + val apps_sum = sum apps 0 + val avrg_inners = handle_inner_timings timings + val new_inners = append_inner_timings avrg_inners inners + in test_troupecheck(append ls1 [gen_sum], append ls2 [apps_sum], new_inners, (n-1)) + end + val (gens, apps, inner_timings) = test_troupecheck([], [],([], [], [], []), 100) + val avrg_timings = handle_inner_timings inner_timings +in + print "generating total:"; + print (average gens); + print "applying args:"; + print (average apps); + print_inners avrg_timings +end + + + diff --git a/troupecheck/timing-experiments/generators.trp b/troupecheck/timing-experiments/generators.trp new file mode 100644 index 0000000..31d711c --- /dev/null +++ b/troupecheck/timing-experiments/generators.trp @@ -0,0 +1,269 @@ +import lists +let fun write x auth = + fwrite ((getStdout auth), x) + + fun init_tc auth rng = + receive [hn ("REQUEST_RNG", senderid) => + let val _ = send (senderid, rng) + in init_tc auth rng end, + + hn ("REQUEST_AUTH", senderid) => + let val _ = send (senderid, auth) + in init_tc auth rng end, + + hn ("UPDATE_RNG", senderid, new_rng) => + let val _ = send(senderid, "done") in + init_tc auth new_rng end] + + fun rec_rng ls = + receive [hn ("REQUEST_RND", senderid) => + let val rnd = random() + val _ = send (senderid, rnd) + in rec_rng (rnd :: ls) + end, + hn ("REQUEST_SEQ", senderid) => + let val _ = send (senderid, (reverse ls)) + in rec_rng [] + end] + val recorder = spawn(fn() => rec_rng []) + val tcp = spawn(fn() => init_tc authority recorder) + + fun save_times ls1 ls2 ls3 ls4= + receive [hn ("ls1", x) => + save_times (x :: ls1) ls2 ls3 ls4, + hn ("ls2", x) => + save_times ls1 (x::ls2) ls3 ls4, + hn ("ls3", x) => + save_times ls1 ls2 (x::ls3) ls4, + hn ("ls4", x) => + save_times ls1 ls2 ls3 (x::ls4), + hn ("get_ls1", sender) => + let val _ = send (sender, ls1) + in save_times [] ls2 ls3 ls4 + end, + hn ("get_ls2", sender) => + let val _ = send (sender, ls2) + in save_times ls1 [] ls3 ls4 + end, + hn ("get_ls3", sender) => + let val _ = send (sender, ls3) + in save_times ls1 ls2 [] ls4 + end, + hn ("get_ls4", sender) => + let val _ = send (sender, ls4) + in save_times ls1 ls2 ls3 [] + end + ] + val state = spawn (fn() => save_times [] [] [] []) + + fun report_error error_reason tco = + let val _ = send (tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + val err_string = case error_reason of + ("cant_generate", tries) => "Couldn't produce an instance that satisfies all strict constraints after " + ^ (toString tries) ^ " tries.\n" + | ("cant_satisfy", tries) => "No valid test could be generated after " ^ (toString tries) ^ " tries.\n" + | ("non_boolean_result", _) => "The property or precondition code returned a non-boolean result.\n" + | ("type_mismatch", _) => "The types' structure doesn't match the property.\n" + | ("illegal_gen_def", _ ) => "Generator is defined wrong - use tuple() or record() to combine generators.\n" + | ("record_mismatch", _) => "the number of names provided for record generation, does not match the number of types provided.\n" + | ("shrinking_looped", _) => "Shrinking looped.\n" + | ("non_string_type", _) => "An element of non-string type found when trying to convert list to string.\n" + in + write "\u001B[31m \nError: " auth; (* Changing the print color to red *) + write (err_string ^ "\u001B[0m") auth; (* Changing the color back *) + exit (auth, 0) end + + fun build_record names vals = + let fun aux r [] [] = r + | aux r (n::ns) (v::vs) = + aux (recordExtend(r, n, v)) ns vs in + aux {} names vals + end + + (* Hardcoded until a tuple from list function is implemented in Troupe - an issue has been raised on GH.*) + fun build_tuple ls = + case ls of + [] => (0) + |[x] => (x) + |[x1,x2] => (x1,x2) + |[x1,x2,x3] => (x1,x2,x3) + |[x1,x2,x3,x4] => (x1,x2,x3,x4) + |[x1,x2,x3,x4,x5] => (x1,x2,x3,x4,x5) + |[x1,x2,x3,x4,x5,x6] => (x1,x2,x3,x4,x5,x6) + |[x1,x2,x3,x4,x5,x6,x7] => (x1,x2,x3,x4,x5,x6,x7) + |[x1,x2,x3,x4,x5,x6,x7,x8] => (x1,x2,x3,x4,x5,x6,x7,x8) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9] => (x1,x2,x3,x4,x5,x6,x7,x8,x9) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10] => (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) + |_ => (2, 3, 4, 5) + + (* Combines a list of individual strings to a single string *) + fun list_to_string ls tco = + foldl (fn (x,y) => if getType x <> "string" then report_error ("non_string_type", 0) tco else y ^ x) "" ls + + fun make_list (f, i) = + case i of + 0 => [] + | _ => (f()) :: (make_list (f, i-1)) + + fun float_gen (low, high) tco size = + let val _ = send (tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + + val _ = send (pid, ("REQUEST_RND", self())) + val x = receive [hn x => x] + + val _ = send (pid, ("REQUEST_RND", self())) + val bool_int = receive [hn x => x] + + val bool = bool_int < (1/2) + + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + + val res = + case (lInf, hInf) of + (true, true) => if bool then x * size else -x * size + | (true, false) => high - (x * size) + | (false, true) => low + (x * size) + | (false, false) => low + (x * (high-low)) + in res + end + + fun int_gen (low, high) tco size = + let val res = floor (float_gen (low, high+1) tco size) + in res + end + + fun one_of ls tco size = + let val idx = (int_gen (1, (length ls)) tco size) + in (nth ls idx) + end + + fun bool_gen tco size = + let val rnd = int_gen (0,1) tco size + val res = if rnd = 0 then false + else true + in res + end + + (* NOTE: Generates only letters (upper and lower case) and numbers. *) + fun char_gen tco size = + let val chars = + ["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", + "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", + "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", + "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", + "0", "1", "2", "3", "4", "5", "6", "7", "8", "9"] + val x = (int_gen (1, ((length chars)-1)) tco size) + in nth chars x + end + + fun label_gen tco size = + newlabel() + + fun tuple_gen ts tco size = + let val start_gen = getTime() + val ts_vals = map (fn x => x tco size) ts + val end_gen = getTime() + val _ = send (state, ("ls1", end_gen - start_gen)) + val start_build = getTime() + val res = build_tuple ts_vals + val end_build = getTime() + val _ = send (state, ("ls2", end_build - start_build)) + in res + end + + (* ns: list of strings - will be used as fieldnames *) + (* ts: list of generators - used to generate values for fields *) + fun rec_gen ns ts tco size = + if (length ns) <> (length ts) then + report_error ("record_mismatch", 0) tco + else + let val ts_vals = map (fn x => x tco size) ts + val res = build_record ns ts_vals + in res + end + + fun labeled_value_gen labels value_gen tco size = + let val inst = value_gen tco size + val lab = one_of labels tco size + in inst raisedTo lab + end + + fun combined_labeled_gen labels gen tco size = + let val labels_to_use = foldl(fn (x,y) => if (bool_gen tco size) then append y [x] else y)[`{}`] labels + val value = gen tco size + val res = foldl (fn (x,y) => y raisedTo x) value labels_to_use + in res + end + + (* NOTE: Generates only strings of letters (upper and lower case) and numbers. *) + fun string_gen tco size = + let val char_ls = list_gen (char_gen) tco size + val string = list_to_string char_ls tco + in string + end + + and list_gen () tco size = + let val len = (int_gen (0, size) tco size) + val gen = generator_gen tco size + val res = make_list ((fn () => gen tco size), len) + in res + end + | list_gen (generator) tco size = + let val len = (int_gen (0, size) tco size) + val res = make_list ((fn () => generator tco size), len) + in res + end + + and generator_gen tco size = + let val inf = 1/0 + val gens_ls = + case (size mod 3) of + 0 => [(float_gen (inf, inf)), (int_gen(inf, inf)), bool_gen, char_gen, string_gen] + | _ => [(float_gen (inf, inf)), (int_gen(inf, inf)), bool_gen, (list_gen(generator_gen tco (size-1))), char_gen, string_gen, + (tuple_gen (list_gen(generator_gen tco (size-1)))), (rec_gen (list_gen(string_gen)) ((generator_gen tco (size-1)))), + (labeled_value_gen (list_gen(string_gen)) (generator_gen tco (size-1)))] + val gen = one_of gens_ls tco size + in gen end + + fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + val inf = 1/0 + fun test_troupecheck_inner 101 = () + | test_troupecheck_inner n = + let val _ = tuple_gen [int_gen(inf, inf), string_gen] tcp n + in test_troupecheck_inner (n+1) + end + + fun test_troupecheck ls1 ls2 0 = (ls1, ls2) + | test_troupecheck ls1 ls2 n = + let val _ = test_troupecheck_inner 0 + val _ = send(state, ("get_ls1", self())) + val gens = receive [hn x => x] + val _ = send(state, ("get_ls2", self())) + val builds = receive [hn x => x] + val sum_gens = sum gens 0 + val sum_builds = sum builds 0 + in test_troupecheck (append ls1 [sum_gens]) (append ls2 [sum_builds]) (n-1) + end + + val (gens, builds) = test_troupecheck [] [] 100 + val avrg_gens = average gens + val avrg_builds = average builds +in + print "generating time:"; + print avrg_gens; + print "building time:"; + print avrg_builds +end + + \ No newline at end of file diff --git a/troupecheck/timing-experiments/internal-shrink-timings.trp b/troupecheck/timing-experiments/internal-shrink-timings.trp new file mode 100644 index 0000000..5559597 --- /dev/null +++ b/troupecheck/timing-experiments/internal-shrink-timings.trp @@ -0,0 +1,607 @@ +import troupecheck +import lists +(* NOTE: for this program to work, troupecheck library file needs to modified to return a tuple on the form: + (<>, <>, <>, <>) + when a failing a test. + The test that is run must always fail at some point. + This program was only made to time different examples of internal shrinking and not meant for further usage.*) + + +let fun eval exp env = + case exp of + ("num", n) => n + | ("var", n) => lookup env n ("unknown variable " ^ n) + | ("add", e1, e2) => (eval e1 env) + (eval e2 env) + | ("sub", e1, e2) => (eval e1 env) - (eval e2 env) + | ("mul", e1, e2) => (eval e1 env) * (eval e2 env) + | ("div", e1, e2) => (eval e1 env) / (eval e2 env) + | _ => print ("Error: ill defined expression"); exit (authority, 1) + + fun execute stmt env = + case stmt of + ("assign", var, exp) => + let val value = eval exp env + in + append [(var, value)] env + end + | ("print", exp) => (()(* print ("from prog: " ^ (toString (eval exp env)) *); env) + + fun remove_nth n [] i = [] + | remove_nth n (x::xs) i = + if n = i then xs + else x :: (remove_nth n xs (i + 1)) + + fun interpret prog = + let fun interpretHelper [] env = env + | interpretHelper (stmt :: rest) env = + let val newEnv = execute stmt env + in + interpretHelper rest newEnv + end + val (stmts, exp) = prog + val last_env = (interpretHelper stmts []) + in + eval exp last_env + end + + fun optimize_prog prog = + let val (stmts, exp) = prog + fun optimize_exp exp = + case exp of + ("num", n) => ("num", n) + | ("var", x) => ("var", x) + | ("add", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1+n2)) + |_ => ("add", (optimize_exp e1), (optimize_exp e2))) + | _ => ("add", (optimize_exp e1), (optimize_exp e2))) + | ("sub", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1-n2)) + |_ => ("sub", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("sub", (optimize_exp e1), (optimize_exp e2))) + | ("mul", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => ("num", (n1*n2)) + |_ => ("mul", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("mul", (optimize_exp e1), (optimize_exp e2))) + | ("div", e1, e2) => + (case e1 of + ("num", n1) => (case e2 of + ("num", n2) => if ((n1 = 0) andalso (n2 = 0)) then ("div", e1, e2) else ("num", (n1/n2)) + |_ => ("div", (optimize_exp e1), (optimize_exp e2)) ) + |_ => ("div", (optimize_exp e1), (optimize_exp e2))) + + fun optimize_stmt stmt = + case stmt of + ("assign", var, exp) => ("assign", var, (optimize_exp exp)) + | ("print", exp) => ("print", (optimize_exp exp)) + in + ((map optimize_stmt stmts), optimize_exp exp) + end + + fun exp_gen ls nesting_level tco size = + let val exp_ts = + if nesting_level = 2 then ["num"] + else (if length ls = 0 then ["num", "add", "sub", "mul", "div"] + else ["var", "num", "add", "sub", "mul", "div"]) + val exp_type = one_of exp_ts tco size + in + case exp_type of + "num" => + let val value = integer(1, inf) tco size in + ("num", value) end + | "var" => + let val value = one_of ls tco size in + ("var", value) end + |"add" => + let val e1 = exp_gen ls (nesting_level+1) tco size + val e2 = exp_gen ls (nesting_level+1) tco size + in + ("add", e1, e2) + end + |"sub" => + let val e1 = exp_gen ls (nesting_level+1) tco size + val e2 = exp_gen ls (nesting_level+1) tco size + in + ("sub", e1, e2) + end + |"mul" => + let val e1 = exp_gen ls (nesting_level+1) tco size + val e2 = exp_gen ls (nesting_level+1) tco size + in + ("mul", e1, e2) + end + |"div" => + let val e1 = exp_gen ls (nesting_level+1) tco size + val e2 = exp_gen ls (nesting_level+1) tco size + in + ("div", e1, e2) + end + end + + fun assign_stmt_gen ls tco size = + let val n = string() tco size + val exp = exp_gen ls 0 tco size + in + ("assign", n, exp) + end + + fun print_stmt_gen ls tco size = + let val exp = exp_gen ls 0 tco size + in + ("print", exp) + end + + fun stmt_gen ls tco size = + let val stmt = one_of ["print", "assign"] tco size + in + case stmt of + "assign" => + let val res = assign_stmt_gen ls tco size in + res end + |"print" => + let val res = print_stmt_gen ls tco size in + res end + end + + fun program_gen tco size = + let val num_of_insts = (integer(0, size) tco size) + fun prog_gen_aux env p 0 = (p, env) + | prog_gen_aux env p i = + let val stmt = stmt_gen env tco size + val newEnv = if stmt.0 = "assign" then (append [stmt.1] env) else env + in + prog_gen_aux newEnv (append p [stmt]) (i-1) + end + val (prog_stmts, last_env) = prog_gen_aux [] [] num_of_insts + val last_exp = exp_gen last_env 0 tco size + val prog = (prog_stmts, last_exp) + in + prog + end + + fun test_prog_shrink prog = + (interpret prog) < 100 + (* -----------Tests shrinking of even numbers *) + fun even_number_gen tco size = + let val int = integer() tco size + in int * 2 + end + fun even_test i = + (i mod 2 = 0) andalso (i < 10) + (* -----------Tests the shrinking of a record with an integer and a string *) + fun record_shrink_test r = + r.theInteger < 50 + + + (* -----------Tests the shrinking of a two strings*) + fun append_always_longer s1 s2 = + let fun string_to_list s = + let fun aux "" acc = acc + | aux s acc = + let val x = substring (s, 0, 1) + val xs = substring (s, 1, 1/0) + in aux xs (append acc [x]) + end + in aux s [] + end + fun string_length s = + length (string_to_list s) + in string_length s1 < string_length (s1 ^ s2) + end + + (* -----------Tests the shrinking of a list of integers *) + fun filter_less ([], _) = [] + | filter_less ((x::xs), p) = + if x < p then append [x] (filter_less (xs, p)) else (filter_less (xs, p)) + + fun filter_greater ([], _) = [] + | filter_greater ((x::xs), p) = + if x > p then append [x] (filter_greater (xs, p)) else (filter_greater (xs, p)) + + + fun my_quicksort [] = [] + | my_quicksort (x::xs) = + let val smaller = my_quicksort(filter_less(xs, x)) + val greater = my_quicksort(filter_greater(xs, x)) in + append (append smaller [x]) (greater) end + fun my_sort_keep_length xs = + length xs = length (my_quicksort(xs)) + + (* -----------Tests the shrinking of a list of strings and a single string *) + fun bad_insert xs x = + if length xs < 10 then append [x] xs else + xs + fun test_bad_insert xs x = + length (bad_insert xs x) = (length xs) + 1 + + (* -----------Tests the shrinking of a float and a one_of statement with a long list *) + fun float_one_of_bad_shrink flt oneOf = + if (flt > 50) andalso (oneOf >= 1) then false else true + + (* Statements to choose from *) + fun program_shrink() = for_all ([program_gen], test_prog_shrink) + fun record_int_string_shrink() = for_all ([(record (["theInteger", "theString"], [integer(), string()]))], record_shrink_test) + fun two_strings_shrink() = for_all ([string(), string()], append_always_longer) + fun integer_list_shrink() = for_all ([list(integer())], my_sort_keep_length) + fun string_and_string_list_shrink() = for_all ([list(string()), string()], test_bad_insert) + fun float_and_one_of_shrink() = for_all ([float(), one_of [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]], float_one_of_bad_shrink) + + + +(* +------------------------------ +INTERNAL SHRINKING + +------------------------------ +*) + fun report_error tup = + print tup.0; + exit (authority, 0) + + fun boolean_check x tco = + () + + fun function_not_done_check p tco = + () +(* +-------------------------------- +UTILS + +Different utility functions that are used across the library. + +-------------------------------- +*) + fun remove_nth n [] i = [] + | remove_nth n (x::xs) i = + if n = i then xs + else x :: (remove_nth n xs (i + 1)) + + fun make_list (f, i) = + case i of + 0 => [] + | _ => (f()) :: (make_list (f, i-1)) + + fun abs_value x = + if x < 0 then -x else x + +(* TODO: handle when arguments are passed to a property that does not take arguments *) + fun apply_args p l tco = + let val _ = send (tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + in case l of + [] => (* this case is only reached if there are no generators to begin with *) + let val _ = boolean_check (p()) tco + val res = p() + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + | (x::xs) => + let val res = foldl (fn (x,y) => function_not_done_check y tco; y x) p l + val _ = boolean_check res tco + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + end + + fun string_to_list s = + let fun aux "" acc = reverse acc + | aux s acc = + let val x = substring (s, 0, 1) + val xs = substring (s, 1, 1/0) in + aux xs (x :: acc) end in + aux s [] end + + (* Combines a list of individual strings to a single string *) + fun list_to_string ls tco = + foldl (fn (x,y) => if getType x <> "string" then report_error ("non_string_type", 0) tco else y ^ x) "" ls + + fun string_length s = + length (string_to_list s) + + fun build_record names vals = + let fun aux r [] [] = r + | aux r (n::ns) (v::vs) = + aux (recordExtend(r, n, v)) ns vs in + aux {} names vals + end + + (* Hardcoded until a tuple from list function is implemented in Troupe - an issue has been raised on GH.*) + fun build_tuple ls = + case ls of + [] => (0) + |[x] => (x) + |[x1,x2] => (x1,x2) + |[x1,x2,x3] => (x1,x2,x3) + |[x1,x2,x3,x4] => (x1,x2,x3,x4) + |[x1,x2,x3,x4,x5] => (x1,x2,x3,x4,x5) + |[x1,x2,x3,x4,x5,x6] => (x1,x2,x3,x4,x5,x6) + |[x1,x2,x3,x4,x5,x6,x7] => (x1,x2,x3,x4,x5,x6,x7) + |[x1,x2,x3,x4,x5,x6,x7,x8] => (x1,x2,x3,x4,x5,x6,x7,x8) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9] => (x1,x2,x3,x4,x5,x6,x7,x8,x9) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10] => (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) + |_ => (2, 3, 4, 5) + + fun dec_nth list idx = + let fun dec_nth_aux [] acc i = reverse acc + | dec_nth_aux (x::xs) acc i = + case i = idx of + true => + let val dec_val = if x <= 1/10000 then 0 else x/(3/2) in + append (reverse (0 :: acc)) xs end + | false => dec_nth_aux xs (x :: acc) (i+1) + in + dec_nth_aux list [] 0 end + + fun zero_nth list idx = + let fun zero_nth_aux [] acc i = reverse acc + | zero_nth_aux (x::xs) acc i = + case i = idx of + true => + append (reverse (0 :: acc)) xs + | false => zero_nth_aux xs (x :: acc) (i+1) + in + zero_nth_aux list [] 0 end + + fun dec_all seq = + let fun dec_all_aux [] i = [] + | dec_all_aux (x::xs) i = + if x = 0 then + dec_all_aux xs (i+1) + else + [(fn () => (zero_nth seq i)), (fn() => [fn () => (dec_nth seq i), fn () => dec_all_aux xs (i+1)])] in + dec_all_aux seq 0 end + + fun seqs_of_seq sequence lengths = + let fun aux seq acc 0 = (reverse acc, seq) + | aux (x::xs) acc n = + aux xs (x :: acc) (n-1) + val (res, _) = (foldl (fn (x,(acc, s)) => + let val (curr_acc, curr_seq) = aux s [] x in + (curr_acc :: acc, curr_seq) end)([], sequence) lengths) + in reverse res + end + + fun cutoff_at list idx = + let fun aux ls acc 0 = reverse acc + | aux (x::xs) acc i = + aux xs (x :: acc) (i-1) in + aux list [] idx end + + fun for_i f y 0 = y + | for_i f y i = for_i f (f (i,y)) (i-1) + + + + + fun init_tc auth rng = + receive [hn ("REQUEST_RNG", senderid) => + let val _ = send (senderid, rng) + in init_tc auth rng end, + + hn ("REQUEST_AUTH", senderid) => + let val _ = send (senderid, auth) + in init_tc auth rng end, + + hn ("UPDATE_RNG", senderid, new_rng) => + let val _ = send(senderid, "done") in + init_tc auth new_rng end] + + fun rec_rng ls = + receive [hn ("REQUEST_RND", senderid) => + let val rnd = random() + val _ = send (senderid, rnd) + in rec_rng (rnd :: ls ) + end, + hn ("REQUEST_SEQ", senderid) => + let val _ = send (senderid, (reverse ls)) + in rec_rng [] + end] + + fun rep_rng ls = + receive [hn ("REQUEST_RND", senderid) => + case ls of + (x::xs) => + let val _ = send (senderid, x) + in rep_rng xs + end + | [] => + let val _ = send (senderid, 0) + in rep_rng ls + end, + hn ("REQUEST_LEFT", senderid) => + let val _ = send (senderid, ls) + in rep_rng [] + end, + hn ("UPDATE_LS", new_ls) => + rep_rng new_ls] + + fun shrink_sized_sequence seqs gens prop pre size left_over_len idx_of_sized tco = + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val _ = send(tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + val cap = ceil (((length (nth seqs (idx_of_sized+1)))-2)/left_over_len )(* number of to remove parts of the sequence *) + val size_ls = reverse (for_i (fn (x,y) => x :: y) [] (left_over_len-1)) + fun aux i = + let val to_remove = reverse (foldl (fn (x,y) => ((i*left_over_len)-x) :: y)[i*left_over_len] size_ls) + val new_seq = foldl (fn (x,y) => remove_nth x y 0) (nth seqs (idx_of_sized+1)) to_remove + val new_seqs = mapi (fn (i, x) => if i = idx_of_sized then new_seq else x) seqs + val new_args = mapi (fn (i, x) => + let val _ = send (pid, ("UPDATE_LS", (nth new_seqs (i+1)))) + val arg = x tco size + in arg + end) gens + in case i = (cap) of + true => + (new_seqs, new_args) + | false => + let val precond_is_met = if (pre <> ()) then (apply_args pre new_args tco) else true + in case (apply_args prop new_args tco) orelse (precond_is_met = false) of + true => aux (i+1) + | false => (new_seqs, new_args) + end + end + in aux 1 + end + + + + fun internal_shrink_aux seqs gens lengths prop pre size counter tco = + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val _ = send(tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + in case seqs of + (x1::x2::x3::xs) => + let val seqs_of_curr = seqs_of_seq (x2()) lengths + val args_and_leftovers = mapi (fn (i, x) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = x tco size + val _ = send (pid, ("REQUEST_LEFT", self())) + val left_overs = receive [hn x => x] + in {arg = arg, left_overs = left_overs} + end) gens + val (test_args_rev, left_over_seqs_rev) = foldl (fn (x, (raws, left_overs)) => (x.arg::raws, x.left_overs::left_overs)) ([],[]) args_and_leftovers + val (test_args, left_over_seqs) = (reverse test_args_rev, reverse left_over_seqs_rev) + val (is_sized_sequence, idx_of_sized, left_over_size, _) = foldl (fn (x,(bool, idx, len, count)) => if (length x > 0) + then (true, count, (length x), (count+1)) + else (bool, idx, len, (count+1))) (false, -1, 0, 0) left_over_seqs + + val (ret_seqs, args) = if is_sized_sequence + then shrink_sized_sequence seqs_of_curr gens prop pre size left_over_size idx_of_sized tco + else (seqs_of_curr, test_args) + val precond_is_met = if (pre <> ()) then (apply_args pre args tco) else true + in + case (apply_args prop args tco) orelse (precond_is_met = false) of + true => internal_shrink_aux (x1::x3()) gens lengths prop pre size counter tco + | false => internal_shrink ret_seqs gens prop pre size (counter+1) tco + end + | (x::xs) => + let val seqs_of_curr = seqs_of_seq (x()) lengths + val test_args = mapi (fn (i, y) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = y tco size + in arg end) gens + val precond_is_met = if (pre <> ()) then (apply_args pre test_args tco) else true + in + case (apply_args prop test_args tco) orelse (precond_is_met = false) orelse (size < 0) of + true => + let val res = mapi (fn (i, y) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = y tco (size+1) + in arg end) gens in + {shrunk_ctx = res, count = counter} end + | false => internal_shrink_aux [x] gens lengths prop pre (size-1) counter tco + + end + end + + and internal_shrink sequences gens prop pre size counter tco = + let val (seqs_comb, seq_lengths_rev) = foldl (fn (x, (seq, lengths)) => ((append seq x), ((length x) :: lengths))) ([], []) sequences + val seq_lengths = reverse seq_lengths_rev + in + if foldl (fn (x,y) => (x = 0) andalso y) true seqs_comb then + internal_shrink_aux [fn () => seqs_comb] gens seq_lengths prop pre size counter tco + else + let val decreased_seqs = dec_all seqs_comb + val dec_seqs_w_root = (fn() => seqs_comb) :: decreased_seqs + val res = internal_shrink_aux dec_seqs_w_root gens seq_lengths prop pre size (counter) tco + in + res end + end + + fun random_shrink_aux sequences generators prop pre success size counter divi tco = + if (counter = 100) orelse (size = 0) then {count = success, size = size, sequences = sequences} else + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val new_size = floor (size/divi) + val (shrunk_args_rev, shrunk_sequences_rev) = + foldl (fn (x, (arg_acc, seq_acc)) => + let val arg = x tco new_size + val _ = send (pid, ("REQUEST_SEQ", self())) + val seq = receive [hn x => x] + in (arg :: arg_acc, seq :: seq_acc) + end) ([],[]) generators + val (shrunk_args, shrunk_sequences) = (reverse shrunk_args_rev, reverse shrunk_sequences_rev) + val precond_is_met = if (pre <> ()) then (apply_args pre shrunk_args tco) else true + in + case (apply_args prop shrunk_args tco) orelse (precond_is_met = false) of + true => random_shrink_aux sequences generators prop pre success size (counter+1) (divi+2) tco + | false => + random_shrink_aux shrunk_sequences generators prop pre (success+1) new_size (0) 2 tco + end + + fun internal_shrinker sequence generators prop pre size counter tco = + let val start_time = getTime() + val rng_recorder = spawn (fn() => rec_rng []) + val _ = send (tco, ("UPDATE_RNG", self(), rng_recorder)) + val _ = receive [hn x => ()] + val res = random_shrink_aux sequence generators prop pre 0 size counter 2 tco + val rng_replayer = spawn (fn() => rep_rng []) + val _ = send (tco, ("UPDATE_RNG", self(), rng_replayer)) + val _ = receive [hn x => ()] + val res = internal_shrink (res.sequences) generators prop pre res.size (res.count) tco + val end_time = getTime() + in + (res, (end_time - start_time)) end + + fun test_shrinking stmt gens prop n = + let fun aux acc 0 = acc + | aux acc i = + let val (_, ctx_seq, size, ctx) = troupecheck [stmt] authority + val _ = print i + val inter_shrink_tco = spawn (fn() => init_tc authority ()) + val pre = () + val int_val = (internal_shrinker ctx_seq gens prop pre size 0 inter_shrink_tco).1 + val newAcc = int_val :: acc + in aux newAcc (i-1) + end + in + aux [] n + end + + (* Statements to choose from *) + fun program_shrink() = for_all ([program_gen], test_prog_shrink) + fun record_int_string_shrink() = for_all ([(record (["theInteger", "theString"], [integer(), string()]))], record_shrink_test) + fun two_strings_shrink() = for_all ([string(), string()], append_always_longer) + fun integer_list_shrink() = for_all ([list(integer())], my_sort_keep_length) + fun string_and_string_list_shrink() = for_all ([list(string()), string()], test_bad_insert) + fun float_and_one_of_shrink() = for_all ([float(), one_of [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]], float_one_of_bad_shrink) + fun even_numbers_shrink() = for_all ([even_number_gen], even_test) + + (* val test_prog = test_shrinking (program_shrink) [program_gen] test_prog_shrink 100 *) + (* val test_int_string = test_shrinking (record_int_string_shrink) [(record (["theInteger", "theString"], [integer(), string()]))] record_shrink_test 100 *) + (* val test_integer_list = test_shrinking (integer_list_shrink) [list(integer())] my_sort_keep_length 100 *) + (* val test_string_stringList = test_shrinking (string_and_string_list_shrink) [list(string()), string()] test_bad_insert 100 *) + (* val test_float_oneOf = test_shrinking (float_and_one_of_shrink) [float(), one_of [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]] float_one_of_bad_shrink 100 *) + val test_even_number = test_shrinking (even_numbers_shrink) [even_number_gen] even_test 100 + + fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end +in + (* print "prog:"; + print (test_prog) *) + (* print "int + string:"; + print (test_int_string) *) + (* print "int list:"; + print (test_integer_list) *) + (* print "string + string list:"; + print (test_string_stringList) *) + (* print "float + one_of:"; + print (test_float_oneOf) *) + print "even numbers:"; + print (test_even_number) + +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/inttest1.trp b/troupecheck/timing-experiments/inttest1.trp new file mode 100644 index 0000000..40c58fc --- /dev/null +++ b/troupecheck/timing-experiments/inttest1.trp @@ -0,0 +1,35 @@ +import troupecheck +import lists +(* NOTE: In order run this the 'troupecheck.trp' library file must be modified, + so that the troupecheck function does not exit the runtime - i.e. replace the call to 'exit(authority, 0)' + with '()', and run make libs, from Troupe directory. + Remember to change back! *) +(* This file times how long it takes takes troupecheck to test a property on two integers, that is always true. + It times this process 100 times and returns the average *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun int_commutative x y = + (x + y) = (y + x) + + fun prop_int_test() = for_all ([integer(), integer()], int_commutative) + + fun test_troupecheck(ls, 0) = ls + | test_troupecheck(ls, n) = + let val startT = getTime() + val _ = troupecheck [prop_int_test] authority + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newList = append ls [elapsedMilliseconds] + val newN = (n-1) + in test_troupecheck(newList, newN) + end +in average (test_troupecheck([], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/inttest2.trp b/troupecheck/timing-experiments/inttest2.trp new file mode 100644 index 0000000..1a216ca --- /dev/null +++ b/troupecheck/timing-experiments/inttest2.trp @@ -0,0 +1,35 @@ +import troupecheck +import lists +(* NOTE: In order run this the 'troupecheck.trp' library file must be modified, + so that the troupecheck function does not exit the runtime - i.e. replace the call to 'exit(authority, 0)' + with '()', and run make libs, from Troupe directory. + Remember to change back! *) +(* This file times how long it takes takes troupecheck to test a property on an integer, that is always true. + It times this process 100 times and returns the average *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun int_test x = + (getType x) = "number" + + fun prop_int_test() = for_all ([integer()], int_test) + + fun test_troupecheck(ls, 0) = ls + | test_troupecheck(ls, n) = + let val startT = getTime() + val _ = troupecheck [prop_int_test] authority + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newList = append ls [elapsedMilliseconds] + val newN = (n-1) + in test_troupecheck(newList, newN) + end +in average (test_troupecheck([], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/inttest3.trp b/troupecheck/timing-experiments/inttest3.trp new file mode 100644 index 0000000..5732fa2 --- /dev/null +++ b/troupecheck/timing-experiments/inttest3.trp @@ -0,0 +1,50 @@ +import lists +(* This file times how long it takes takes troupe to cons an element in front of a list. *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun float_gen (low, high) tco size = + let val x = random() + + val bool_int = random () + + val bool = bool_int < (1/2) + + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + + val res = + case (lInf, hInf) of + (true, true) => if bool then x * size else -x * size + | (true, false) => high - (x * size) + | (false, true) => low + (x * size) + | (false, false) => low + (x * (high-low)) + in res + end + + fun int_gen (low, high) tco size = + let val res = floor (float_gen (low, high+1) tco size) + in res + end + + val inf = 1/0 + + fun test_int(timings, 0) = timings + | test_int(timings, n) = + let val startT = getTime() + val _ = int_gen(inf, inf) () n + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newTimings = append timings [elapsedMilliseconds] + val newN = (n-1) + in test_int(newTimings, newN) + end +in average (test_int([], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/patterntest.trp b/troupecheck/timing-experiments/patterntest.trp new file mode 100644 index 0000000..9a7ade6 --- /dev/null +++ b/troupecheck/timing-experiments/patterntest.trp @@ -0,0 +1,59 @@ +import lists +(* This file times how long it takes takes troupe to cons an element in front of a list. *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun float_gen (low, high) tco size = + let val x = random() + + val bool_int = random () + + val bool = bool_int < (1/2) + + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + + val res = + case (lInf, hInf) of + (true, true) => if bool then x * size else -x * size + | (true, false) => high - (x * size) + | (false, true) => low + (x * size) + | (false, false) => low + (x * (high-low)) + in res + end + + val inf = 1/0 + val low = inf + val high = inf + + fun test_pattern(timings, 0) = timings + | test_pattern(timings, n) = + let val x = random() + + val bool_int = random () + + val bool = bool_int < (1/2) + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + val startT = getTime() + val res = + case (lInf, hInf) of + (true, true) => if bool then x * n else -x * n + | (true, false) => high - (x * n) + | (false, true) => low + (x * n) + | (false, false) => low + (x * (high-low)) + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newTimings = append timings [elapsedMilliseconds] + val newN = (n-1) + in test_pattern(newTimings, newN) + end +in average (test_pattern([], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/reversetest.trp b/troupecheck/timing-experiments/reversetest.trp new file mode 100644 index 0000000..98aa46c --- /dev/null +++ b/troupecheck/timing-experiments/reversetest.trp @@ -0,0 +1,25 @@ +import lists +(* This file times how long it takes takes trouep to reverse a list of two elements (the choice sequence in TC has length 2 after generating an integer). + It times this done 100 times and returns the average *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun test_cons(ls, timings, 0) = timings + | test_cons(ls, timings, n) = + let val startT = getTime() + val _ = reverse ls + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newTimings = append timings [elapsedMilliseconds] + val newN = (n-1) + in test_cons(ls, newTimings, newN) + end +in average (test_cons([random(), random()], [], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/send-receivetest.trp b/troupecheck/timing-experiments/send-receivetest.trp new file mode 100644 index 0000000..70f082b --- /dev/null +++ b/troupecheck/timing-experiments/send-receivetest.trp @@ -0,0 +1,41 @@ +import lists +(* This file times how long it takes takes troupe to send and receive elements between processes. + Average time ~0.10 milliseconds *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun rec_rng ls = + receive [hn ("REQUEST_RND", senderid) => + let val rnd = random() + val _ = send (senderid, rnd) + in rec_rng (rnd :: ls) + end] + val recorder = spawn(fn() => rec_rng []) + + fun test () = + let val _ = send(recorder, ("REQUEST_RND", self())) + val x = receive [hn x => x] + in x + end + + fun test_cons(timings, 0) = timings + | test_cons(timings, n) = + let val startT = getTime() + val res = test() + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newTimings = append timings [elapsedMilliseconds] + val newN = (n-1) + in test_cons(newTimings, newN) + end +in + print (average (test_cons([], 1000))); + exit(authority, 0) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/shrink_comparisons.trp b/troupecheck/timing-experiments/shrink_comparisons.trp new file mode 100644 index 0000000..fcf90a8 --- /dev/null +++ b/troupecheck/timing-experiments/shrink_comparisons.trp @@ -0,0 +1,592 @@ +import troupecheck +import lists +(* NOTE: for this program to work, troupecheck library file needs to modified to return a tuple on the form: + (<>, <>, <>, <>) + when a failing a test. + The test that is run must always fail at some point. + This program was only made to test internal vs. external shrinking, and not meant for further usage.*) +let fun record_shrink_test r = + r.theInteger < 50 + fun prop_record_shrink() = for_all ([(record (["theInteger", "theString"], [integer(), string()]))], record_shrink_test) + +(* +------------------------------ +INTERNAL SHRINKING + +------------------------------ +*) + fun report_error tup = + print tup.0; + exit (authority, 0) + + fun boolean_check x tco = + () + + fun function_not_done_check p tco = + () +(* +-------------------------------- +UTILS + +Different utility functions that are used across the library. + +-------------------------------- +*) + fun remove_nth n [] i = [] + | remove_nth n (x::xs) i = + if n = i then xs + else x :: (remove_nth n xs (i + 1)) + + fun make_list (f, i) = + case i of + 0 => [] + | _ => append [f()] (make_list (f, i-1)) + + +(* TODO: handle when arguments are passed to a property that does not take arguments *) + fun apply_args p l tco = + let val _ = send (tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + in case l of + [] => (* this case is only reached if there are no generators to begin with *) + let val _ = boolean_check (p()) tco + val res = p() + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + | (x::xs) => + let val res = foldl (fn (x,y) => function_not_done_check y tco; y x) p l + val _ = boolean_check res tco + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + end + + fun string_to_list s = + let fun aux "" acc = acc + | aux s acc = + let val x = substring (s, 0, 1) + val xs = substring (s, 1, 1/0) in + aux xs (append acc [x]) end in + aux s [] end + + (* Combines a list of individual strings to a single string *) + fun list_to_string ls tco = + foldl (fn (x,y) => if getType x <> "string" then report_error ("non_string_type", 0) tco else y ^ x) "" ls + + fun string_length s = + length (string_to_list s) + + fun build_record names vals = + let fun aux r [] [] = r + | aux r (n::ns) (v::vs) = + aux (recordExtend(r, n, v)) ns vs in + aux {} names vals + end + + (* Hardcoded until a tuple from list function is implemented in Troupe - an issue has been raised on GH.*) + fun build_tuple ls = + case ls of + [] => (0) + |[x] => (x) + |[x1,x2] => (x1,x2) + |[x1,x2,x3] => (x1,x2,x3) + |[x1,x2,x3,x4] => (x1,x2,x3,x4) + |[x1,x2,x3,x4,x5] => (x1,x2,x3,x4,x5) + |[x1,x2,x3,x4,x5,x6] => (x1,x2,x3,x4,x5,x6) + |[x1,x2,x3,x4,x5,x6,x7] => (x1,x2,x3,x4,x5,x6,x7) + |[x1,x2,x3,x4,x5,x6,x7,x8] => (x1,x2,x3,x4,x5,x6,x7,x8) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9] => (x1,x2,x3,x4,x5,x6,x7,x8,x9) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10] => (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) + |_ => (2, 3, 4, 5) + + fun dec_nth list idx = + let fun dec_nth_aux [] acc i = acc + | dec_nth_aux (x::xs) acc i = + case i = idx of + true => + let val dec_val = if x <= 1/10000 then 0 else x/(3/2) in + append (append acc [dec_val]) xs end + | false => dec_nth_aux xs (append acc [x]) (i+1) + in + dec_nth_aux list [] 0 end + + fun zero_nth list idx = + let fun zero_nth_aux [] acc i = acc + | zero_nth_aux (x::xs) acc i = + case i = idx of + true => + append (append acc [0]) xs + | false => zero_nth_aux xs (append acc [x]) (i+1) + in + zero_nth_aux list [] 0 end + + fun dec_all seq = + let fun dec_all_aux [] i = [] + | dec_all_aux (x::xs) i = + if x = 0 then + dec_all_aux xs (i+1) + else + [(fn () => (zero_nth seq i)), (fn() => [fn () => (dec_nth seq i), fn () => dec_all_aux xs (i+1)])] in + dec_all_aux seq 0 end + + fun seqs_of_seq sequence lengths = + let fun aux seq acc 0 = (acc, seq) + | aux (x::xs) acc n = + aux xs (append acc [x]) (n-1) + val (res, _) = (foldl (fn (x,(acc, s)) => + let val (curr_acc, curr_seq) = aux s [] x in + (append acc [curr_acc], curr_seq) end)([], sequence) lengths) + in res + end + + fun cutoff_at list idx = + let fun aux ls acc 0 = acc + | aux (x::xs) acc i = + aux xs (append acc [x]) (i-1) in + aux list [] idx end + + fun for_i f y 0 = y + | for_i f y i = for_i f (f (i,y)) (i-1) +(* +-------------------------------- +SHRINKING + +Works by first using random shrinking when a failing example has been found (shrink & random_shrink_aux). +Random shrinking means simply generating new test cases with gradually smaller size, to find a case smaller than the original one. This rarely produces a minmal result. +The smallest randomly shrunk instance is then further shrunk using internal shrinking. (internal_shrink & internal_shrink_aux) +Internal shrinking means keeping track of all random decision made during generation, and then re-generating with smaller "random" decisions. + +This part of the code also contains the functionality for recording all random decisions, and replaying these random decisions (rec_rng & rep_rng). +All of these functions are spawned and then requests or updates may be send to them, so that the correct RNG's are used at different points in the code. + +-------------------------------- +*) + fun init_tc auth rng = + receive [hn ("REQUEST_RNG", senderid) => + let val _ = send (senderid, rng) + in init_tc auth rng end, + + hn ("REQUEST_AUTH", senderid) => + let val _ = send (senderid, auth) + in init_tc auth rng end, + + hn ("UPDATE_RNG", senderid, new_rng) => + let val _ = send(senderid, "done") in + init_tc auth new_rng end] + + + fun rec_rng ls = + receive [hn ("REQUEST_RND", senderid) => + let val rnd = random() + val _ = send (senderid, rnd) + in rec_rng (rnd :: ls) + end, + hn ("REQUEST_SEQ", senderid) => + let val _ = send (senderid, (reverse ls)) + in rec_rng [] + end] + + fun rep_rng ls = + receive [hn ("REQUEST_RND", senderid) => + case ls of + (x::xs) => + let val _ = send (senderid, x) + in rep_rng xs + end + | [] => + let val _ = send (senderid, 0) + in rep_rng ls + end, + hn ("REQUEST_LEFT", senderid) => + let val _ = send (senderid, ls) + in rep_rng [] + end, + hn ("UPDATE_LS", new_ls) => + rep_rng new_ls] + + fun shrink_sized_sequence seqs gens prop pre size left_over_len idx_of_sized tco = + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val _ = send(tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + val cap = ceil (((length (nth seqs (idx_of_sized+1)))-2)/left_over_len )(* number of to remove parts of the sequence *) + val size_ls = for_i (fn (x,y) => append y [x]) [] (left_over_len-1) + fun aux i = + let val to_remove = foldl (fn (x,y) => append y [(i*left_over_len)-x])[i*left_over_len] size_ls + val new_seq = foldl (fn (x,y) => remove_nth x y 0) (nth seqs (idx_of_sized+1)) to_remove + val new_seqs = mapi (fn (i, x) => if i = idx_of_sized then new_seq else x) seqs + val new_args = mapi (fn (i, x) => + let val _ = send (pid, ("UPDATE_LS", (nth new_seqs (i+1)))) + val arg = x tco size + in arg + end) gens + in case i = (cap) of + true => + (new_seqs, new_args) + | false => + let val precond_is_met = if (pre <> ()) then (apply_args pre new_args tco) else true + in case (apply_args prop new_args tco) orelse (precond_is_met = false) of + true => aux (i+1) + | false => (new_seqs, new_args) + end + end + in aux 1 + end + + + + fun internal_shrink_aux seqs gens lengths prop pre size counter tco = + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val _ = send(tco, ("REQUEST_AUTH", self())) + val auth = receive [hn x => x] + in case seqs of + (x1::x2::x3::xs) => + let val seqs_of_curr = seqs_of_seq (x2()) lengths + val args_and_leftovers = mapi (fn (i, x) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = x tco size + val _ = send (pid, ("REQUEST_LEFT", self())) + val left_overs = receive [hn x => x] + in {arg = arg, left_overs = left_overs} + end) gens + val (test_args, left_over_seqs) = foldl (fn (x, (raws, left_overs)) => (append raws [x.arg], append left_overs [x.left_overs])) ([],[]) args_and_leftovers + (* val ret_seqs = mapi (fn (i,x) => + if (length x) = 0 then (nth seqs_of_curr (i+1)) + else cutoff_at (nth seqs_of_curr (i+1)) ((nth lengths (i+1))-(length x))) left_over_seqs *) + val (is_sized_sequence, idx_of_sized, left_over_size, _) = foldl (fn (x,(bool, idx, len, count)) => if (length x > 0) + then (true, count, (length x), (count+1)) + else (bool, idx, len, (count+1))) (false, -1, 0, 0) left_over_seqs + + val (ret_seqs, args) = if is_sized_sequence + then shrink_sized_sequence seqs_of_curr gens prop pre size left_over_size idx_of_sized tco + else (seqs_of_curr, test_args) + val precond_is_met = if (pre <> ()) then (apply_args pre args tco) else true + in + case (apply_args prop args tco) orelse (precond_is_met = false) of + true => internal_shrink_aux (x1::x3()) gens lengths prop pre size counter tco + | false => internal_shrink ret_seqs gens prop pre size (counter+1) tco + end + | (x::xs) => + let val seqs_of_curr = seqs_of_seq (x()) lengths + val test_args = mapi (fn (i, y) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = y tco size + in arg end) gens + val precond_is_met = if (pre <> ()) then (apply_args pre test_args tco) else true + in + case (apply_args prop test_args tco) orelse (precond_is_met = false) orelse (size < 0) of + true => + let val res = mapi (fn (i, y) => + let val _ = send (pid, ("UPDATE_LS", (nth seqs_of_curr (i+1)))) + val arg = y tco (size+1) + in arg end) gens in + {shrunk_ctx = res, count = counter} end + | false => internal_shrink_aux [x] gens lengths prop pre (size-1) counter tco + + end + end + + and internal_shrink sequences gens prop pre size counter tco = + let val (seqs_comb, seq_lengths) = foldl (fn (x, (seq, lengths)) => ((append seq x), (append lengths [(length x)]))) ([], []) sequences + in + if foldl (fn (x,y) => (x = 0) andalso y) true seqs_comb then + internal_shrink_aux [fn () => seqs_comb] gens seq_lengths prop pre size counter tco + else + let val decreased_seqs = dec_all seqs_comb + val dec_seqs_w_root = append [fn() => seqs_comb] decreased_seqs + val res = internal_shrink_aux dec_seqs_w_root gens seq_lengths prop pre size (counter) tco + in + res end + end + + fun random_shrink_aux sequences generators prop pre success size counter divi tco = + if (counter = 100) orelse (size = 0) then {count = success, size = size, sequences = sequences} else + let val _ = send(tco, ("REQUEST_RNG", self())) + val pid = receive [hn x => x] + val new_size = floor (size/divi) + val (shrunk_args, shrunk_sequences) = + foldl (fn (x, (arg_acc, seq_acc)) => + let val arg = x tco new_size + val _ = send (pid, ("REQUEST_SEQ", self())) + val seq = receive [hn x => x] + in (append arg_acc [arg], append seq_acc [seq]) + end) ([],[]) generators + val precond_is_met = if (pre <> ()) then (apply_args pre shrunk_args tco) else true + in + case (apply_args prop shrunk_args tco) orelse (precond_is_met = false) of + true => random_shrink_aux sequences generators prop pre success size (counter+1) (divi+2) tco + | false => + random_shrink_aux shrunk_sequences generators prop pre (success+1) new_size (0) 2 tco + end + + fun internal_shrinker sequence generators prop pre size counter tco = + let val start_time = getTime() + val rng_recorder = spawn (fn() => rec_rng []) + val _ = send (tco, ("UPDATE_RNG", self(), rng_recorder)) + val _ = receive [hn x => ()] + val res = random_shrink_aux sequence generators prop pre 0 size counter 2 tco + val rng_replayer = spawn (fn() => rep_rng []) + val _ = send (tco, ("UPDATE_RNG", self(), rng_replayer)) + val _ = receive [hn x => ()] + val res = internal_shrink (res.sequences) generators prop pre res.size (res.count) tco + val end_time = getTime() + in + (res, (end_time-start_time)) + end + +(* +------------------------------ +EXTERNAL SHRINKING + +------------------------------ +*) + fun abs_value x = + if x < 0 then -x else x + + fun list_to_string ls = + foldl (fn (x,y) => if getType x <> "string" then report_error ("non_string_type", 0) else y ^ x) "" ls + + fun apply_args p l = + case l of + [] => boolean_check (p()); p() (* this case is only reached if there are no generators to beign with*) + | (x::xs) => + let val res = foldl (fn (x,y) => function_not_done_check y; y x) p l in + boolean_check res; + res + end + + fun shrink_sized_aggregate vals builder rec = + case rec.state of + "init" => + let val init_shrink_idx = 0 + val new_vals = mapi (fn (i, x) => + if i = init_shrink_idx then (x.shrinker {state = "init", curr = x.raw, prev = x.raw}) + else {state = "init", curr = x.raw, prev = x.raw}) vals + val new_raw_vals = map (fn x => x.curr) new_vals + val new_state = if (foldl (fn (x,y) => (x.state = "done") andalso y) true new_vals) then "done" else "cont" + val shrink_idx = if (nth new_vals (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + in + {state = new_state, curr = (builder new_raw_vals), prev = rec.curr, next_shrink_info = new_vals, shrink_idx = shrink_idx} + end + | "cont" => + let val init_shrink_idx = rec.shrink_idx + val new_vals = mapi (fn (i, x) => + if i = init_shrink_idx then x.shrinker (nth rec.next_shrink_info (i+1)) + else (nth rec.next_shrink_info (i+1))) vals + val new_raw_vals = map (fn x => x.curr) new_vals + val new_state = if (foldl (fn (x,y) => (x.state = "done") andalso y) true new_vals) then "done" else "cont" + val shrink_idx = if (nth new_vals (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + in + {state = new_state, curr = (builder new_raw_vals), prev = rec.curr, next_shrink_info = new_vals, shrink_idx = shrink_idx} + end + | "done" => + rec + | "rollback" => + let val init_shrink_idx = rec.shrink_idx + fun rollback_aux (i, x) = + if i = init_shrink_idx then + (let val val_to_shrink = {(nth rec.next_shrink_info (i+1)) with state = "rollback"} + in + x.shrinker val_to_shrink + end ) + else (nth rec.next_shrink_info (i+1)) + val rollback_args = mapi rollback_aux vals + val new_raw_vals = map (fn x => x.curr) rollback_args + val new_state = if (foldl (fn (x,y) => (x.state = "done") andalso y) true rollback_args) then "done" else "cont" + val shrink_idx = if (nth rollback_args (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + in + {state = new_state, curr = (builder new_raw_vals), prev = rec.curr, next_shrink_info = rollback_args, shrink_idx = shrink_idx} + end + + fun shrink_float rec = + let val rec_checked = if rec.curr = 0 then {rec with state = "done"} else rec + val curr_val = rec_checked.curr + in + case rec_checked.state of + "rollback" => + {state = "done", curr = rec_checked.prev, prev = rec_checked.curr} + |"done" => + rec_checked + | _ => + let val new_raw_val = if (abs_value curr_val)-1 <= 0 then 0 else curr_val-1 + in + {state = "cont", curr = new_raw_val, prev = rec_checked.curr} + end + end + + fun shrink_int rec = + let val interim = shrink_float rec + in + {interim with curr = floor(interim.curr)} + end + + fun remove_nth n [] i = [] + | remove_nth n (x::xs) i = + if n = i then xs + else x :: (remove_nth n xs (i + 1)) + + fun shrink_list shrinkers rec = + if (rec.curr = []) andalso (rec.state <> "rollback") then {rec with state = "done", prev = rec.curr, idx = 0} + else + case rec.state of + "init" => + let val removeIdx = (length (rec.curr)) - 1 + val newList = remove_nth removeIdx rec.curr 0 + val new_shrinkers = remove_nth removeIdx shrinkers 0 + val next_state = if length newList = 0 then "cont_elem" else "cont_size" + in + {state = next_state, curr = newList, prev = rec.curr, idx = removeIdx, shrinkers = new_shrinkers, prev_shrinkers = shrinkers} + end + | "cont_size" => + let val remove_idx = (rec.idx - 1) + val next_state = if remove_idx <= 0 then "cont_elem" else "cont_size" + val new_list = remove_nth remove_idx rec.curr 0 + val new_shrinkers = remove_nth remove_idx rec.shrinkers 0 + in + {state = next_state, curr = new_list, prev = rec.curr, idx = remove_idx, shrinkers = new_shrinkers, prev_shrinkers = rec.shrinkers} + end + | "cont_elem" => + let val interim_list = mapi (fn (i, x) => (nth rec.shrinkers (i+1)){state = "init", curr = x, prev = x}) rec.curr + val next_state = if (foldl (fn (x,y) => (x.state = "done") andalso y) true interim_list) then "done" else "cont_elem" + val new_list = map (fn x => x.curr) interim_list + in + {state = next_state, curr = new_list, prev = rec.curr, idx = rec.idx, shrinkers = rec.shrinkers, prev_shrinkers = rec.prev_shrinkers} + end + | "rollback" => + if (length rec.curr) = (length rec.prev) then + {state = "done", curr = rec.prev, prev = rec.curr, idx = rec.idx, shrinkers = rec.prev_shrinkers, prev_shrinkers = rec.shrinkers} (* TODO: this loops an unecesary amount of times *) + else + {state = "cont_size", curr = rec.prev, prev = rec.curr, idx = rec.idx, shrinkers = rec.prev_shrinkers, prev_shrinkers = rec.shrinkers} + | "done" => + rec + + fun shrink_char rec = + let val chars = + ["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", + "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", + "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", + "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", + "0", "1", "2", "3", "4", "5", "6", "7", "8", "9"] + val rec_checked = if rec.curr = "a" then {rec with state = "done"} else rec + val curr_val = rec_checked.curr in + case rec_checked.state of + "rollback" => + {state = "done", curr = rec.prev, prev = rec.curr, idx = rec.idx} + | "done" => + rec_checked + | "init" => + let val index_of_new = (lookup chars rec.curr 2) - 1 + val new_char = nth chars index_of_new + in + {state = "cont", curr = new_char, prev = rec.curr, idx = index_of_new} + end + | _ => + let val index_of_new = rec.idx-1 + val new_char = nth chars index_of_new + in + {state = "cont", curr = new_char, prev = rec.curr, idx = index_of_new} + end + end + + fun shrink_string rec = + let val rec_checked = if rec.state = "init" then {rec with next_shrink_info = 0} else rec in + case rec_checked.state of + "cont_elem" => + {rec_checked with state = "done"} (* TODO: Should actually shrink characters *) + | _ => + let val ls_curr = string_to_list rec_checked.curr + val ls_prev = string_to_list rec_checked.prev + val shrinkers = map (fn _ => shrink_char) ls_curr + val interim_res = + shrink_list shrinkers {state = rec_checked.state, + curr = ls_curr, + prev = ls_prev, + idx = rec_checked.next_shrink_info, + shrinkers = shrinkers, + prev_shrinkers = shrinkers} + val new_curr = list_to_string interim_res.curr + val new_prev = list_to_string interim_res.prev + + val res = {state = interim_res.state, curr = new_curr, prev = new_prev, next_shrink_info = interim_res.idx} + in + res + end + end + + fun args_shrink args = + case args.state of + "rollback" => + let val init_shrink_idx = args.shrink_idx + val rollbackReadyArgs = mapi (fn (i, x) => if (x.state = "done") orelse (i<>init_shrink_idx) then x else {x with state = "rollback"}) args.args + val argsRolledBack = mapi (fn (i, x) => if i = init_shrink_idx then (nth args.shrinkers (i+1)) x else x) rollbackReadyArgs + val nextState = if (foldl (fn (x,y) => (x.state = "done") andalso y) true argsRolledBack) then "done" else "cont" + val shrink_idx = if (nth argsRolledBack (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + in + {state = nextState, args = argsRolledBack, shrinkers = args.shrinkers, shrink_idx = shrink_idx} + end + | "done" => + args + | _ => + let val init_shrink_idx = args.shrink_idx + val newArgs = mapi (fn (i, x) => if i = init_shrink_idx then ((nth args.shrinkers (i+1)) x) else x) args.args + val nextState = if (foldl (fn (x,y) => (x.state = "done") andalso y) true newArgs) then "done" else "cont" + val shrink_idx = if (nth newArgs (init_shrink_idx+1)).state = "done" then init_shrink_idx+1 else init_shrink_idx + + in + {state = nextState, args = newArgs, shrinkers = args.shrinkers, shrink_idx = shrink_idx} + end + + fun shrink_aux args prop pre counter = + if counter = 100 then report_error ("shrinking_looped", 0) else + let val shrunk_args = args_shrink args + val shrunk_args_raw = map (fn x => x.curr) shrunk_args.args + val precond_is_met = if (pre <> ()) then (apply_args pre shrunk_args_raw) else true + + in case (apply_args prop shrunk_args_raw) orelse (precond_is_met = false) of + true => shrink_aux (args_shrink {state = "rollback", args = shrunk_args.args, shrinkers = args.shrinkers, shrink_idx = args.shrink_idx}) prop pre (counter) + | false => + if shrunk_args.state = "done" then {shrunk_ctx = shrunk_args_raw, count = counter} else shrink_aux shrunk_args prop pre (counter+1) end + + fun external_shrinker args prop pre = + let val start_time = getTime() + val shrinkers = map (fn x => x.shrinker) args + val args_shrink_ready = map (fn x => {state = "init", curr = x.raw, prev = x.raw}) args + val args_rec = {state = "init", args = args_shrink_ready, shrinkers = shrinkers, shrink_idx = 0} + val res = shrink_aux args_rec prop pre 0 + val end_time = getTime() + in (res, (end_time - start_time)) end + + + + fun test_shrinking n = + let fun aux acc 0 = acc + | aux acc i = + let val (_, ctx_seq, size, ctx) = troupecheck [prop_record_shrink] authority + val ctx_n = nth ctx 1 + val ts_vals = [{raw = ctx_n.theInteger, shrinker = shrink_int}, {raw = ctx_n.theString, shrinker = shrink_string} ] + val ext_shrink_val = [{raw = ctx_n, shrinker = shrink_sized_aggregate ts_vals (build_record ["theInteger", "theString"])}] + val inter_shrink_tco = spawn (fn() => init_tc authority ()) + val pre = () + val ext_val = (external_shrinker ext_shrink_val record_shrink_test pre).1 + val int_val = (internal_shrinker ctx_seq [(record (["theInteger", "theString"], [integer(), string()]))] record_shrink_test pre size 0 inter_shrink_tco).1 + + val ext = append acc.ext [ext_val] + val inter = append acc.inter [int_val] + in aux {ext, inter} (i-1) + end + in + aux {ext = [], inter = []} n + end + val test = test_shrinking 100 + val ext_sum = foldl (fn (x,y) => x+y) 0 test.ext + val inter_sum = foldl (fn (x,y) => x+y) 0 test.inter + val ext_mean = ext_sum/100 + val inter_mean = inter_sum/100 +in + print ("external timings: " ^ (toString test.ext)); + print ("mean: " ^ (toString ext_mean)); + print ("internal timings: " ^ (toString test.inter)); + print ("mean: " ^ (toString inter_mean)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/strjointest.trp b/troupecheck/timing-experiments/strjointest.trp new file mode 100644 index 0000000..4961dfb --- /dev/null +++ b/troupecheck/timing-experiments/strjointest.trp @@ -0,0 +1,24 @@ +import lists +(* This file times how long it takes takes troupe to cons an element in front of a list. *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun test_strjoin(str, timings, 0) = timings + | test_strjoin(str, timings, n) = + let val startT = getTime() + val newStr = str ^ "d" + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newTimings = append timings [elapsedMilliseconds] + val newN = (n-1) + in test_strjoin(newStr, newTimings, newN) + end +in average (test_strjoin("", [], 100)) +end \ No newline at end of file diff --git a/troupecheck/timing-experiments/tc-nosendreceive.trp b/troupecheck/timing-experiments/tc-nosendreceive.trp new file mode 100644 index 0000000..140e5ec --- /dev/null +++ b/troupecheck/timing-experiments/tc-nosendreceive.trp @@ -0,0 +1,515 @@ +import lists + +(* +-------------------------------- +INIT FUNCTION + +To be called when starting out testing + +-------------------------------- +*) + +(* +-------------------------------- +PRINTING TO CONSOLE + +Simple functions for more convenient printing to console. + +-------------------------------- +*) +let fun write x auth = + fwrite ((getStdout auth), x) + + fun args_toString args = + let fun aux_toString acc (x0::x1::xs) = aux_toString (acc ^ (toString x0) ^ ", ") (x1::xs) + | aux_toString acc (x::xs) = acc ^ (toString x) in + aux_toString "" args end + +(* +-------------------------------- +ERROR HANDLING + +Handles the printing of appropriate error messages for errors that may occur in the use of TroupeCheck. + +-------------------------------- +*) + fun report_error error_reason tco = + let val auth = authority + val err_string = case error_reason of + ("cant_generate", tries) => "Couldn't produce an instance that satisfies all strict constraints after " + ^ (toString tries) ^ " tries.\n" + | ("cant_satisfy", tries) => "No valid test could be generated after " ^ (toString tries) ^ " tries.\n" + | ("non_boolean_result", _) => "The property or precondition code returned a non-boolean result.\n" + | ("type_mismatch", _) => "The types' structure doesn't match the property.\n" + | ("illegal_gen_def", _ ) => "Generator is defined wrong - use tuple() or record() to combine generators.\n" + | ("record_mismatch", _) => "the number of names provided for record generation, does not match the number of types provided.\n" + | ("shrinking_looped", _) => "Shrinking looped.\n" + | ("non_string_type", _) => "An element of non-string type found when trying to convert list to string.\n" + in + write "\u001B[31m \nError: " auth; (* Changing the print color to red *) + write (err_string ^ "\u001B[0m") auth; (* Changing the color back *) + exit (auth, 0) end + + fun boolean_check x tco = + if (getType x)<>"boolean" then report_error ("non_boolean_result", 0) tco else () + + fun function_not_done_check p tco = + if (getType p)<>"function" then report_error ("type_mismatch", 0) tco else () +(* +-------------------------------- +UTILS + +Different utility functions that are used across the library. + +-------------------------------- +*) + fun remove_nth n [] i = [] + | remove_nth n (x::xs) i = + if n = i then xs + else x :: (remove_nth n xs (i + 1)) + + fun make_list (f, i) = + case i of + 0 => [] + | _ => append [f()] (make_list (f, i-1)) + + +(* TODO: handle when arguments are passed to a property that does not take arguments *) + fun apply_args p l tco = + let val auth = authority + in case l of + [] => (* this case is only reached if there are no generators to begin with *) + let val _ = boolean_check (p()) tco + val res = p() + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + | (x::xs) => + let val res = foldl (fn (x,y) => function_not_done_check y tco; y x) p l + val _ = boolean_check res tco + val _ = blockdecl auth + in declassify (res, auth, `{}`) + end + end + + fun string_to_list s = + let fun aux "" acc = acc + | aux s acc = + let val x = substring (s, 0, 1) + val xs = substring (s, 1, 1/0) in + aux xs (append acc [x]) end in + aux s [] end + + (* Combines a list of individual strings to a single string *) + fun list_to_string ls tco = + foldl (fn (x,y) => if getType x <> "string" then report_error ("non_string_type", 0) tco else y ^ x) "" ls + + fun string_length s = + length (string_to_list s) + + fun report_fail_reason rec noOfTests tco = + let val auth = authority in + case rec.failReason of + "false_prop" => + write "\nFailure at input: " auth; + write (args_toString rec.ctx) auth; + write ("\nAfter running: " ^ (toString (noOfTests - rec.remTests + 1)) ^ " test(s)\n") auth + end + + fun build_record names vals = + let fun aux r [] [] = r + | aux r (n::ns) (v::vs) = + aux (recordExtend(r, n, v)) ns vs in + aux {} names vals + end + + (* Hardcoded until a tuple from list function is implemented in Troupe - an issue has been raised on GH.*) + fun build_tuple ls = + case ls of + [] => (0) + |[x] => (x) + |[x1,x2] => (x1,x2) + |[x1,x2,x3] => (x1,x2,x3) + |[x1,x2,x3,x4] => (x1,x2,x3,x4) + |[x1,x2,x3,x4,x5] => (x1,x2,x3,x4,x5) + |[x1,x2,x3,x4,x5,x6] => (x1,x2,x3,x4,x5,x6) + |[x1,x2,x3,x4,x5,x6,x7] => (x1,x2,x3,x4,x5,x6,x7) + |[x1,x2,x3,x4,x5,x6,x7,x8] => (x1,x2,x3,x4,x5,x6,x7,x8) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9] => (x1,x2,x3,x4,x5,x6,x7,x8,x9) + |[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10] => (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) + |_ => (2, 3, 4, 5) + + fun dec_nth list idx = + let fun dec_nth_aux [] acc i = acc + | dec_nth_aux (x::xs) acc i = + case i = idx of + true => + let val dec_val = if x <= 1/10000 then 0 else x/(3/2) in + append (append acc [dec_val]) xs end + | false => dec_nth_aux xs (append acc [x]) (i+1) + in + dec_nth_aux list [] 0 end + + fun zero_nth list idx = + let fun zero_nth_aux [] acc i = acc + | zero_nth_aux (x::xs) acc i = + case i = idx of + true => + append (append acc [0]) xs + | false => zero_nth_aux xs (append acc [x]) (i+1) + in + zero_nth_aux list [] 0 end + + fun dec_all seq = + let fun dec_all_aux [] i = [] + | dec_all_aux (x::xs) i = + if x = 0 then + dec_all_aux xs (i+1) + else + [(fn () => (zero_nth seq i)), (fn() => [fn () => (dec_nth seq i), fn () => dec_all_aux xs (i+1)])] in + dec_all_aux seq 0 end + + fun seqs_of_seq sequence lengths = + let fun aux seq acc 0 = (acc, seq) + | aux (x::xs) acc n = + aux xs (append acc [x]) (n-1) + val (res, _) = (foldl (fn (x,(acc, s)) => + let val (curr_acc, curr_seq) = aux s [] x in + (append acc [curr_acc], curr_seq) end)([], sequence) lengths) + in res + end + + fun cutoff_at list idx = + let fun aux ls acc 0 = acc + | aux (x::xs) acc i = + aux xs (append acc [x]) (i-1) in + aux list [] idx end + + fun for_i f y 0 = y + | for_i f y i = for_i f (f (i,y)) (i-1) +(* +-------------------------------- +SHRINKING + +Works by first using random shrinking when a failing example has been found (shrink & random_shrink_aux). +Random shrinking means simply generating new test cases with gradually smaller size, to find a case smaller than the original one. This rarely produces a minmal result. +The smallest randomly shrunk instance is then further shrunk using internal shrinking. (internal_shrink & internal_shrink_aux) +Internal shrinking means keeping track of all random decision made during generation, and then re-generating with smaller "random" decisions. + +This part of the code also contains the functionality for recording all random decisions, and replaying these random decisions (rec_rng & rep_rng). +All of these functions are spawned and then requests or updates may be send to them, so that the correct RNG's are used at different points in the code. + +-------------------------------- +*) + fun random_shrink_aux generators prop pre success size counter divi tco = + if (counter = 1000) orelse (size = 0) then {count = success, size = size} else + let val new_size = floor (size/divi) + val (shrunk_args) = + foldl (fn (x, (arg_acc)) => + let val arg = x tco new_size + in (append arg_acc [arg]) + end) ([]) generators + val precond_is_met = if (pre <> ()) then (apply_args pre shrunk_args tco) else true + in + case (apply_args prop shrunk_args tco) orelse (precond_is_met = false) of + true => random_shrink_aux generators prop pre success size (counter+1) (divi+2) tco + | false => + random_shrink_aux generators prop pre (success+1) new_size (0) 2 tco + end + + fun shrink generators prop pre size counter tco = + let val res = random_shrink_aux generators prop pre 0 size counter 2 tco + in + res + end +(* +-------------------------------- +GENERATORS + +Contains generators for Troupe's built-in types. All generators must return a single instance of the type they generate, +and take a 'size' argument as the very last argument. +This size will be given to all generators in the generation of test cases (and shrinking). +Generators that take more arguments, will need to have these passed along to them before passing the generator to the testing facilities +(convenience functions for this are supplied later). + +It is recommended that all user defined generators only make use of pre-defined generators or their matching convenience functions +for random decisions (i.e. a call to float_gen/float() or int_gen/integer()), instead of having to send and receive the correct messages to the RNG threads. +However, it can be done if the users wishes to and understands what is going on. + +-------------------------------- +*) + + fun float_gen (low, high) tco size = + let val x = random() + + val bool_int = random () + + val bool = bool_int < (1/2) + + val lInf = low = 1/0 (* check for inf *) + val hInf = high = 1/0 + + val res = + case (lInf, hInf) of + (true, true) => if bool then x * size else -x * size + | (true, false) => high - (x * size) + | (false, true) => low + (x * size) + | (false, false) => low + (x * (high-low)) + in res + end + + fun int_gen (low, high) tco size = + let val res = floor (float_gen (low, high+1) tco size) + in res + end + + fun one_of ls tco size = + let val idx = (int_gen (1, (length ls)) tco size) + in (nth ls idx) + end + + fun bool_gen tco size = + let val rnd = int_gen (0,1) tco size + val res = if rnd = 0 then false + else true + in res + end + + (* NOTE: Generates only letters (upper and lower case) and numbers. *) + fun char_gen tco size = + let val chars = + ["a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", + "n", "o", "p", "q", "r", "s", "t", "u", "v", "w", "x", "y", "z", + "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", + "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", + "0", "1", "2", "3", "4", "5", "6", "7", "8", "9"] (* length: 62 *) + val x = (int_gen (1, (62-1)) tco size) + in nth chars x + end + + fun label_gen tco size = + newlabel() + + (* ts: list of generators - used to generate values for fields *) + (* NOTE: Hardcoded for tuple of up to 10 elements - see build_tuple in 'UTILS' *) + fun tuple_gen ts tco size = + let val ts_vals = map (fn x => x tco size) ts + in build_tuple ts_vals + end + + (* ns: list of strings - will be used as fieldnames *) + (* ts: list of generators - used to generate values for fields *) + fun rec_gen ns ts tco size = + if (length ns) <> (length ts) then + report_error ("record_mismatch", 0) tco + else + let val ts_vals = map (fn x => x tco size) ts + val res = build_record ns ts_vals + in res + end + + fun labeled_value_gen labels value_gen tco size = + let val inst = value_gen tco size + val lab = one_of labels tco size + in inst raisedTo lab + end + + fun combined_labeled_gen labels gen tco size = + let val labels_to_use = foldl(fn (x,y) => if (bool_gen tco size) then append y [x] else y)[`{}`] labels + val value = gen tco size + val res = foldl (fn (x,y) => y raisedTo x) value labels_to_use + in res + end + + (* NOTE: Generates only strings of letters (upper and lower case) and numbers. *) + fun string_gen tco size = + let val length = (int_gen (0, size) tco size) + fun string_aux acc 0 = acc + | string_aux acc i = string_aux ((char_gen tco size) ^ acc) (i-1) + val string = (string_aux "" length) + in string + end + + and list_gen () tco size = + let val len = (int_gen (0, size) tco size) + val gen = generator_gen tco size + val res = make_list ((fn () => gen tco size), len) + in res + end + | list_gen (generator) tco size = + let val len = (int_gen (0, size) tco size) + val res = make_list ((fn () => generator tco size), len) + in res + end + + and generator_gen tco size = + let val inf = 1/0 + val gens_ls = + case (size mod 3) of + 0 => [(float_gen (inf, inf)), (int_gen(inf, inf)), bool_gen, char_gen, string_gen] + | _ => [(float_gen (inf, inf)), (int_gen(inf, inf)), bool_gen, (list_gen(generator_gen tco (size-1))), char_gen, string_gen, + (tuple_gen (list_gen(generator_gen tco (size-1)))), (rec_gen (list_gen(string_gen)) ((generator_gen tco (size-1)))), + (labeled_value_gen (list_gen(string_gen)) (generator_gen tco (size-1)))] + val gen = one_of gens_ls tco size + in gen end + +(* +-------------------------------- +CORE FUNCTIONALITY + +Handles preparing the recorder RNG, running the tests, calling the shrinker, and reporting the results to the user. + +-------------------------------- +*) + fun core_forall (generators, prop, 0, size, pre, cap, tco) = {failReason = (), ctx = (), remTests = 0, size = size} + |core_forall (generators, prop, i, size, pre, cap, tco) = + let val auth = authority + val (args) = foldl (fn (x, (arg_acc)) => + let val arg = x tco size + in (append arg_acc [arg]) + end) ([]) generators + in + case pre of + () => + if (apply_args prop args tco) then + let val _ = write "." auth + in core_forall (generators, prop, i-1, size+1, pre, cap, tco) + end + else + let val _ = write "!" auth + in {failReason = "false_prop", ctx = args, remTests = i, size = size} + end + | _ => + if (apply_args pre args tco) then + if (apply_args prop args tco) then (write "." auth; core_forall (generators, prop, i-1, size+1, pre, cap, tco)) + else + let val _ = write "!" auth + in {failReason = "false_prop", ctx = args, remTests = i, size = size} + end + else + let val _ = write "x" auth + in if (size = cap) andalso (i*5 = cap) then report_error ("cant_satisfy", size) tco + else if size = cap then {failReason = (), ctx = (), remTests = i, size = size} + else core_forall (generators, prop, i, size+1, pre, cap, tco) + end + end + + fun run_tests (generators, p, to_shrink, noOfTests) auth = + let val (prop, pre) = + case p of + (x,y) => (x,y) + | x => (x, ()) + val tco = () + val res = core_forall (generators, prop, noOfTests, 0, pre, (noOfTests*5), tco) in + case res.failReason of + () => write ("\u001B[1m \u001B[32m \nSuccess: \u001B[0mPassed all " ^ (toString noOfTests) ^ " test(s).\n") auth; true + |_ => + report_fail_reason res noOfTests tco; + if to_shrink then + (write ("\u001B[1m\u001B[34mShrinking\u001B[0m:") auth; + let val shrink_res = shrink generators prop pre res.size 0 tco in + write "\nFailing test case was shrunk to:\n" auth; + write (args_toString shrink_res.shrunk_ctx) auth; + write ("\nAfter " ^ (toString shrink_res.count) ^ " iterations.\n") auth; + false + end) + else + false + end + + fun for_all (generators, p) auth = run_tests (generators, p, true, 100) auth + | for_all (generators, p, noOfTests) auth = run_tests (generators, p, true, noOfTests) auth + + fun for_all_noshrink (generators, p) auth = run_tests (generators, p, false, 100) auth + | for_all_noshrink (generators, p, noOfTests) auth = run_tests (generators, p, false, noOfTests) auth + + fun troupecheck props auth = + let val n = toString (length props) + fun troupecheck_aux [] i = ()(* exit(auth, 0) *) + | troupecheck_aux (x::xs) i = + let val _ = write ("\nRunning test " ^ (toString i) ^ " of " ^ n ^ ":\n") auth + val res = x() auth + in troupecheck_aux xs (i+1) end + in troupecheck_aux props 1 + end + +(* +-------------------------------- +CONVENIENCE FUNCTIONS + +These are functions that make it easier for the user to make use of the different generators, and define their own generators. + +-------------------------------- +*) + val inf = 1 / 0 + fun integer () = int_gen(inf, inf) + | integer (l, h) = int_gen(l, h) + + fun pos_integer () = integer(0, inf) + + fun neg_integer () = integer(inf, -1) + + fun float () = float_gen(inf, inf) + | float (h, l) = float_gen(h, l) + + fun pos_float () = float(0, inf) + + fun neg_float () = float(inf, 0) + + fun boolean () = bool_gen + + fun list () = list_gen () + |list (type) = list_gen (type) + + fun string () = string_gen + + fun char () = char_gen + + fun generator() = generator_gen + + fun tuple (ts) = tuple_gen ts + + fun labeled_value (ls, gen) = labeled_value_gen ls gen + + fun combined_labeled_value (ls, gen) = combined_labeled_gen ls gen + + fun label() = label_gen + + fun record (ns, ts) = rec_gen ns ts + + + + + fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun tuple_test (number, string) = + getType number = "number" + + fun prop_tuple_test() = for_all ([tuple([integer(), string()])], tuple_test) + + fun int_test x = + (getType x) = "number" + + fun prop_int_test() = for_all ([integer()], int_test) + + fun test_troupecheck(ls, 0) = ls + | test_troupecheck(ls, n) = + let val startT = getTime() + val _ = troupecheck [prop_tuple_test] authority + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newList = append ls [elapsedMilliseconds] + val newN = (n-1) + in test_troupecheck(newList, newN) + end +in + average (test_troupecheck([], 100)) +end diff --git a/troupecheck/timing-experiments/tupletest.trp b/troupecheck/timing-experiments/tupletest.trp new file mode 100644 index 0000000..7829769 --- /dev/null +++ b/troupecheck/timing-experiments/tupletest.trp @@ -0,0 +1,35 @@ +import troupecheck +import lists +(* NOTE: In order run this the 'troupecheck.trp' library file must be modified, + so that the troupecheck function does not exit the runtime - i.e. replace the call to 'exit(authority, 0)' + with '()', and run make libs, from Troupe directory. + Remember to change back! *) +(* This file times how long it takes takes troupecheck to test a property on tuples, that is always true. + It times this process 100 times and returns the average *) +let fun sum [] acc = acc + | sum (x::xs) acc = + sum xs (acc+x) + + fun average ls = + let val len = length ls + val sum_ls = sum ls 0 + in (sum_ls/len) + end + + fun tuple_test (number, string) = + getType number = "number" + + fun prop_tuple_test() = for_all ([tuple([integer(), string()])], tuple_test) + + fun test_troupecheck(ls, 0) = ls + | test_troupecheck(ls, n) = + let val startT = getTime() + val _ = troupecheck [prop_tuple_test] authority + val endT = getTime() + val elapsedMilliseconds = endT - startT + val newList = append ls [elapsedMilliseconds] + val newN = (n-1) + in test_troupecheck(newList, newN) + end +in average (test_troupecheck([], 100)) +end \ No newline at end of file