fuzzer_runner.pl

conflicting_solutions(contradiction_found, solution(_)).

conflicting_solutions(solution(_), contradiction_found).

do_halt :-
    ( fuzzer_found_error(_) ->
    findall(FailedTest, fuzzer_found_error(FailedTest), FailedTests),
    format("Fuzzing tests failed: ~w", [FailedTests]),
    halt(1)
    ; nl, write('All fuzzing tests passed.'),nl,
    halt(0)
).

error_other_than_wd_occurred :-
    check_error_occured(Error, _),
    Error \== well_definedness_error,
    format("Error occurred during fuzzing: ~w~n", [Error]).

fuzzy_verify_smt_solver :-
    % check SMT solver results for consistency with ProB excluding erroneous results
    get_fuzzing_timeout(FTO),
    fuzz(verify_smt_solutions_with_prob, 1, 100000, FTO, prob_ast_pred([]), ErrorFound),
    handle_error_found(fuzzy_verify_smt_solver, ErrorFound).

fuzzy_verify_smt_solver_large_conj_with_ids :-
    % check SMT solver results for consistency with ProB excluding erroneous results
    get_fuzzing_timeout(FTO),
    fuzz(verify_smt_solutions_with_prob, 1, 1000, FTO, prob_ast_conj([noString,conjuncts:50,id]), ErrorFound),
    handle_error_found(fuzzy_verify_smt_solver, ErrorFound).

fuzzy_verify_smt_solver_large_disj_with_ids :-
    % check SMT solver results for consistency with ProB excluding erroneous results
    get_fuzzing_timeout(FTO),
    fuzz(verify_smt_solutions_with_prob, 1, 1000, FTO, prob_ast_conj([noString,disjuncts:50,id]), ErrorFound),
    handle_error_found(fuzzy_verify_smt_solver, ErrorFound).

fuzzy_verify_smt_solver_no_error_but_wd :-
    % check that the SMT solver does not throw any error but well-definedness errors
    get_fuzzing_timeout(FTO),
    fuzz(smt_no_error_but_wd, 1, 100000, FTO, prob_ast_pred([]), ErrorFound),
    handle_error_found(fuzzy_verify_smt_solver_no_error_but_wd, ErrorFound).

fuzzy_verify_smt_solver_no_sets :-
    % check SMT solver results for consistency with ProB excluding erroneous results
    get_fuzzing_timeout(FTO),
    fuzz(verify_smt_solutions_with_prob, 1, 100000, FTO, prob_ast_pred([noSet]), ErrorFound),
    handle_error_found(fuzzy_verify_smt_solver_no_sets, ErrorFound).

fuzzy_verify_smt_solver_no_strings :-
    % check SMT solver results for consistency with ProB excluding erroneous results
    get_fuzzing_timeout(FTO),
    fuzz(verify_smt_solutions_with_prob, 1, 100000, FTO, prob_ast_pred([noString]), ErrorFound),
    handle_error_found(fuzzy_verify_smt_solver_no_strings, ErrorFound).

fuzzy_verify_smt_solver_no_strings_not_wd :-
    % check SMT solver results for consistency with ProB excluding erroneous results
    get_fuzzing_timeout(FTO),
    fuzz(verify_smt_solutions_with_prob, 1, 100000, FTO, prob_ast_pred([not-well-defined,noString]), ErrorFound),
    handle_error_found(fuzzy_verify_smt_solver_no_strings, ErrorFound).

fuzzy_verify_smt_solver_no_strings_with_ids :-
    % check SMT solver results for consistency with ProB excluding erroneous results
    get_fuzzing_timeout(FTO),
    fuzz(verify_smt_solutions_with_prob, 1, 100000, FTO, prob_ast_pred([id,noString]), ErrorFound),
    handle_error_found(fuzzy_verify_smt_solver, ErrorFound).

get_bindings(P, Bindings) :-
    find_identifier_uses(P, [], Ids),
    findall(bind(Id,_), member(Id, Ids), Bindings).

get_fuzzing_timeout(FTO) :-
    preferences:get_preference(time_out, TO),
    FTO is TO * 2.

handle_error_found(TestName, ErrorFound) :-
    ( ErrorFound
    -> assertz(fuzzer_found_error(TestName))
    ; true
).

init_pref :-
    startup_prob,
    external_functions:reset_argv,
    prob_cli:set_prefs,
    % load empty machine
    absolute_file_name(prob_examples('public_examples/CSPB/LTSMin/Empty.mch'), EmptyPath, []),
    b_load_machine_from_file(EmptyPath),
    b_machine_precompile.

is_acceptable_error(Res) :-
    Res == error,
    ( check_error_occured(internal_error(b_compiler),_)
    ; check_error_occured(check_ast_typing,_)
    ; is_wd_error(Res)
).

is_wd_error(Res) :-
    Res == error,
    check_error_occured(well_definedness_error, _).

no_conflict_due_to_annotation(Pred) :-
    get_preference(sat_supported_interpreter, Pref),
    temporary_set_preference(sat_supported_interpreter, false),
    solve_predicate(Pred, _, Sol),
    temporary_set_preference(sat_supported_interpreter, true),
    solve_predicate(Pred, _, AnnotatedSol),
    set_preference(sat_supported_interpreter, Pref),
    \+ conflicting_solutions(Sol, AnnotatedSol),
    \+ error_other_than_wd_occurred.

prob_accepts_result(_, Res) :-
    % skip erroneous constraints or timeout
    ( Res == error
    ; Res == time_out
    ),
    !.

prob_accepts_result(Pred, solution([])) :-
    solve_clean_predicate(Pred, _, Res),
    ( Res = solution([])
    ; Res = no_solution_found(enumeration_warning(_,_,_,_,_))
    ; Res = time_out
    ; is_acceptable_error(Res)
    ), !.

prob_accepts_result(Pred, solution(Bindings)) :-
    ground(Bindings),
    solve_clean_predicate(Pred, Bindings, Res),
    ( Res = solution(_)
    ; Res = no_solution_found(enumeration_warning(_,_,_,_,_))
    ; Res == time_out
    ; is_acceptable_error(Res)
    ), !.

prob_accepts_result(Pred, SolverSolution) :-
    SolverSolution == contradiction_found,
    solve_clean_predicate(Pred, _, Res),
    ( Res == contradiction_found
    ; Res = no_solution_found(enumeration_warning(_,_,_,_,_))
    ; Res == time_out
    ; is_acceptable_error(Res)
    ), !.

prob_accepts_result(Pred, SolverSolution) :-
    SolverSolution = no_solution_found(enumeration_warning(_,_,_,_,_)),
    solve_clean_predicate(Pred, _, Res),
    ( Res = no_solution_found(enumeration_warning(_,_,_,_,_))
    ; Res = solution(_)
    ; Res == contradiction_found
    ; Res == time_out
    ; is_acceptable_error(Res)
    ), !.

reset_state :-
    retractall(fuzzer_found_error(_)).

run_all_tests :-
    reset_state,
    test2 , test5 , test6 , test7 , test8 , test9 ,
    test10 , test11 , test12 , test13 , test14 , test15 , test16 , test17 ,
    test18 , test19 , test20 , test21 , test22 , test23 , test24 , test25 ,
    %test26 , test27 ,
    test29 , test30.

run_fuzz_tests :-
    init_pref ,
    % generate fresh state at each start by using system time
    now(R),
    setrand(R),
    run_all_tests.

run_tests :-
    run_fuzz_tests,
    do_halt.

smt_no_error_but_wd(Pred) :-
    reset_errors,
    cdclt_solve_predicate(Pred, _, Res),
    ( Res == error
    -> is_acceptable_error(Res)
    ; true
).

solve_clean_predicate(Pred, Bindings, Res) :-
    reset_errors,
    clean_up_pred(Pred, _, CPred),
    solve_predicate(CPred, Bindings, Res).

test1 :-
    init_pref,
    get_fuzzing_timeout(FTO),
    fuzz(test1_aux,1,10000,FTO,prob_ast_pred([setSize:3]),ErrorFound),
    handle_error_found(test1, ErrorFound).

test10 :-
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:and_equality,3,10000,FTO,
    prob_value_boolean([]):prob_value_boolean([]):var,ErrorFound),
    handle_error_found(test10, ErrorFound).

test11 :-
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:or_eq_obj,3, 10000,FTO,
    prob_value_boolean([]):prob_value_boolean([]):var,ErrorFound),
    handle_error_found(test11, ErrorFound).

test12 :-
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:equality_objects,3,10000,FTO,
    prob_value_set(set(integer([]),[setSize:4]),[]):
    prob_value_set(set(integer([]),[setSize:4]),[]):
    var,ErrorFound),
    handle_error_found(test12, ErrorFound).

test13 :-
    init_pref,
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:subset_test,4,10000,FTO,
    prob_value_set(string([]),[]):
    prob_value_set(string([]),[]):var:var,ErrorFound),
    handle_error_found(test13, ErrorFound).

test14 :-
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:subset_test,4,10000,FTO,
    prob_value_set(set(integer([]),[setSize:2]),[list]):
    prob_value_set(set(integer([]),[setSize:3]),[list]):var:var,ErrorFound),
    handle_error_found(test14, ErrorFound).

test15 :-
    init_pref ,
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:subset_strict_test,4,10000,FTO,
    prob_value_set(integer([]),[avl]):
    prob_value_set(integer([]),[avl]):var:var,ErrorFound),
    handle_error_found(test15, ErrorFound).

test16 :-
    init_pref ,
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:subset_strict_test,4,10000,FTO,
    prob_value_set(set(string([]),[setBound:20]),[avl,setBound:20]):
    prob_value_set(set(string([]),[setBound:20]),[list,setBound:40]):var:var,ErrorFound),
    handle_error_found(test16, ErrorFound).

test17 :-
    init_pref,
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:membership_test_wf,4,10000,FTO,
    prob_value_set(set(string([]),[setBound:5]),[]):
    prob_value_set(string([]),[list,setBound:5]):var:var,ErrorFound),
    handle_error_found(test17, ErrorFound).

test18 :-
    init_pref,
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:membership_test_wf,4,10000,FTO,
    prob_value_set(integer([]),[]):
    prob_value_integer([]):var:var,ErrorFound),
    handle_error_found(test18, ErrorFound).

test19 :-
    init_pref,
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:membership_test_wf,4,10000,FTO,
    prob_value_set(set(integer([]),[setBound:20]),[avl,setBound:60]):
    prob_value_set(integer([]),[list,setBound:20]):var:var,ErrorFound),
    handle_error_found(test19, ErrorFound).

test1_aux(Predicate) :-
    reset_errors,
    get_bindings(Predicate, BindList),
    preferences:get_preference(time_out, TO),
    time_out(
    (b_test_boolean_expression_cs(Predicate,BindList,[],'Fuzzer',0) ;
    b_not_test_boolean_expression_cs(Predicate,BindList,[],'Fuzzer (negated)',0) ;
    get_error(well_definedness_error,_)),
    TO,
    Res),
    ( Res == success
    ; Res == time_out
    ),
    \+ error_other_than_wd_occurred.

test2 :-
    init_pref,
    get_fuzzing_timeout(FTO),
    % don't generate ASTs with identifiers since b_compute_expression_nowf/4 evaluates constraints but does not find solutions
    fuzz(test2_aux,1,20000,FTO,prob_ast_expr([]),ErrorFound),
    handle_error_found(test2, ErrorFound).

test20 :-
    init_pref,
    get_fuzzing_timeout(FTO),
    fuzz(test20_aux,1,10000,FTO,prob_value_any([small]),ErrorFound),
    handle_error_found(test20, ErrorFound).

test20_aux(AnyValue) :-
    reset_errors,
    kernel_equality:equality_objects(AnyValue,AnyValue,Res),
    Res == pred_true,
    \+ error_other_than_wd_occurred.

test21 :-
    init_pref ,
    get_fuzzing_timeout(FTO),
    fuzz(test21_aux,1,10000,FTO,prob_ast_integer([]),ErrorFound),
    handle_error_found(test21, ErrorFound).

test21_aux(IntegerNode) :-
    generate(mutation(IntegerNode:prob_ast_int_expr),Mutation) ,
    b_compute_expression_nowf(IntegerNode,[],[],Value,'Fuzzer Integer',1) ,
    b_compute_expression_nowf(Mutation,[],[],MutationValue,'Fuzzer Integer',2) , ! ,
    kernel_objects:equal_object(Value,MutationValue),
    \+ error_other_than_wd_occurred.

test22 :-
    init_pref ,
    get_fuzzing_timeout(FTO),
    fuzz(test1_aux,1,10000,FTO,prob_ast_pred(equal,[record]),ErrorFound),
    handle_error_found(test22, ErrorFound).

test23 :-
    get_fuzzing_timeout(FTO),
    fuzz(kernel_objects:add_element,3,10000,FTO,
    prob_value_integer([]):prob_value_set(integer([]),[]):var,ErrorFound),
    handle_error_found(test23, ErrorFound).

test24 :-
    get_fuzzing_timeout(FTO),
    fuzz(kernel_objects:add_element,3,10000,FTO,
    prob_value_set(string([]),[setSize:2]):prob_value_set(set(string([]),[setSize:5]),[setSize:3]):var,ErrorFound),
    handle_error_found(test24, ErrorFound).

test25 :-
    init_pref ,
    get_fuzzing_timeout(FTO),
    fuzz(test25_aux,1,10000,FTO,
    % generate two elements of any but the same type, therefore generate a list
    prob_value_set(any([noset]),[list,setSize:2,size:2,not-well-defined-values]),ErrorFound),
    handle_error_found(test25, ErrorFound).

test25_aux([Value1,Value2]) :-
    ( kernel_objects:equal_object(Value1,Value2)
    ; kernel_objects:not_equal_object(Value1,Value2)),
    \+ error_other_than_wd_occurred.

test29 :-
    init_pref ,
    get_fuzzing_timeout(FTO),
    fuzz(test29_aux,1,10000,FTO,prob_ast_int_expr([nonEmpty]),ErrorFound),
    handle_error_found(test29, ErrorFound).

test29_aux(AST) :-
    generate(detype(AST),DetypedAST) ,
    btypechecker:typecheck_result_init(_ErrorsIn,_Delayed,_Identifiers,TRStart),
    btypechecker:btype(fuzzing,DetypedAST,env_empty,_NType,TypedAST,TRStart,TRout) ,
    btypechecker:typecheck_result_get_errors(TRout,Errors),
    (var(Errors) -> true ; format('TYPE ERRORS: ~w~n',[Errors]),translate:print_bexpr(AST),nl,fail),
    (( b_compute_expression_nowf(AST,[],[],Res1,'Fuzzer AST',1) ,
    b_compute_expression_nowf(TypedAST,[],[],Res2,'Fuzzer AST',2) ,
    kernel_objects:equal_object(Res1,Res2) )
    ; get_error(well_definedness_error,_)),
    \+ error_other_than_wd_occurred.

test2_aux(Expression) :-
    reset_errors,
    get_bindings(Expression, BindList),
    preferences:get_preference(time_out, TO),
    time_out(
    (b_compute_expression_nowf(Expression,BindList,[],_R,'Fuzzer',0) ;
    get_error(well_definedness_error,_)),
    TO,
    Res),
    ( Res == success
    ; Res == time_out
    ),
    \+ error_other_than_wd_occurred.

test30 :-
    init_pref ,
    get_fuzzing_timeout(FTO),
    fuzz(test30_aux,1,1000,FTO,prob_ast_pred([nonEmpty,setBound:10,alph,noQuantifier]),ErrorFound),
    handle_error_found(test30, ErrorFound).

test30_aux(AST) :-
    % remove types and re-run typechecker and check that either both ASTs succeed or both fail
    %nl,nl,print('Test 30 : '),translate:print_bexpr(AST),nl,
    generate(detype(AST),DetypedAST) ,
    % TO DO: detype sometimes removes types for empty set or empty sequence or sequence_extension([]) ...
    % TO DO: find a better entry point predicate in btypechecker or provide it there
    btypechecker:typecheck_result_init(_ErrorsIn,_Delayed,_Identifiers,TRStart),
    btypechecker:btype(fuzzing,DetypedAST,openenv(_,env_empty),_Type,TypedAST,TRStart,TRout) ,
    btypechecker:typecheck_result_get_errors(TRout,Errors),
    (var(Errors) -> true ; format('TYPE ERRORS: ~w~n',[Errors]),translate:print_bexpr(AST),nl,fail),
    %print('Re-typed: '),translate:print_bexpr(TypedAST),nl,
    ( b_test_boolean_expression_cs(AST,[],[],'Fuzzer AST',1) ,
    b_test_boolean_expression_cs(TypedAST,[],[],'Fuzzer AST',2)
    ; b_not_test_boolean_expression_cs(AST,[],[],'Fuzzer AST (negated)',1) ,
    b_not_test_boolean_expression_cs(TypedAST,[],[],'Fuzzer AST (negated)',1)
    ; get_error(well_definedness_error,_)
    ),
    \+ error_other_than_wd_occurred.

test5 :-
    init_pref,
    get_fuzzing_timeout(FTO),
    % same as test2 but considering larger sets
    fuzz(test2_aux,1,2000,FTO,prob_ast_set_expr([setBound:1000]),ErrorFound),
    handle_error_found(test2, ErrorFound).

test6 :-
    init_pref,
    get_fuzzing_timeout(FTO),
    % same as test2 but considering larger sequences
    fuzz(test2_aux,1,2000,FTO,prob_ast_seq_expr([setBound:100]),ErrorFound),
    handle_error_found(test2, ErrorFound).

test7 :-
    get_fuzzing_timeout(FTO),
    fuzz(kernel_equality:equality_objects,3,10000,FTO,
    prob_value_integer([]):prob_value_integer([]):var,ErrorFound),
    handle_error_found(test7, ErrorFound).

test8 :-
    get_fuzzing_timeout(FTO),
    fuzz(test8_aux,2,10000,FTO,
    prob_value_string([size:111]):
    prob_value_string([size:110]),ErrorFound),
    handle_error_found(test8, ErrorFound).

test8_aux(String1,String2) :-
    kernel_equality:equality_objects(String1,String2,Res) ,
    Res = pred_false,
    \+ error_other_than_wd_occurred.

test9 :-
    get_fuzzing_timeout(FTO),
    fuzz(test8_aux,2,10000,FTO,
    prob_value_set(integer([]),[setSize:53]):
    prob_value_set(integer([]),[setSize:102]),ErrorFound),
    handle_error_found(test9, ErrorFound).

test_automated_kodkod_annotation :-
    get_fuzzing_timeout(FTO),
    fuzz(kodkod_annotator:annotate_kodkod_constraints, 3, 1000, FTO, fixed(greedy):prob_ast_pred([]):var,ErrorFound1),
    handle_error_found(test_automated_kodkod_annotation1, ErrorFound1),
    !,
    fuzz(kodkod_annotator:annotate_kodkod_constraints, 3, 1000, FTO, fixed(greedy):prob_ast_expr([]):var,ErrorFound2),
    handle_error_found(test_automated_kodkod_annotation2, ErrorFound2),
    !,
    fuzz(kodkod_annotator:annotate_kodkod_constraints, 3, 1000, FTO, fixed(preferred):prob_ast_pred([]):var,ErrorFound3),
    handle_error_found(test_automated_kodkod_annotation3, ErrorFound3),
    !,
    fuzz(kodkod_annotator:annotate_kodkod_constraints, 3, 1000, FTO, fixed(preferred):prob_ast_expr([]):var,ErrorFound4),
    handle_error_found(test_automated_kodkod_annotation4, ErrorFound4),
    !.

test_automated_kodkod_annotation_solving :-
    get_fuzzing_timeout(FTO),
    fuzz(user:no_conflict_due_to_annotation, 1, 1000, FTO, prob_ast_pred([]),ErrorFound),
    handle_error_found(test_automated_kodkod_annotation_solving, ErrorFound),
    !.

verify_smt_solutions_with_prob(Pred) :-
    reset_errors,
    cdclt_solve_predicate(Pred, SolvedPred, Solution),
    !,
    prob_accepts_result(SolvedPred, Solution).