1 | % (c) 2009-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(test_typechecker,[run_typecheck_testcase/2]). | |
6 | ||
7 | :- use_module(library(codesio)). | |
8 | :- use_module(library(file_systems)). | |
9 | ||
10 | :- use_module(probsrc(bsyntaxtree)). | |
11 | :- use_module(probsrc(btypechecker)). | |
12 | :- use_module(probsrc(bmachine_structure)). | |
13 | :- use_module(probsrc(bmachine_construction)). | |
14 | :- use_module(probsrc(parsercall)). | |
15 | :- use_module(probsrc(tools)). | |
16 | :- use_module(probsrc(translate),[pretty_type/2]). | |
17 | ||
18 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
19 | % typechecker-test framework | |
20 | ||
21 | run_typecheck_testcase(Filename,Type) :- | |
22 | run_testcase(Filename,Filename,Type,Verdicts), | |
23 | nl,print_verdicts(Verdicts,*), | |
24 | summarized_verdict(Verdicts,V), | |
25 | !, | |
26 | (V==pass -> print('All tests passed\n') ; print('Test failed\n'),fail). | |
27 | ||
28 | print_verdicts([],_). | |
29 | print_verdicts([verdict(Testname,Subname,Verdict)|Rest],Before) :- | |
30 | (Before=Testname -> true ; write(Testname),write(':'),nl), | |
31 | format('~t~q~10|: ~q~n',[Subname,Verdict]), | |
32 | print_verdicts(Rest,Testname). | |
33 | ||
34 | summarized_verdict(Vs,Sum) :- summarized_verdict2(Vs,pass,Sum). | |
35 | summarized_verdict2([],V,V). | |
36 | summarized_verdict2([verdict(_,_,V)|Rest],Old,New) :- | |
37 | (V==pass -> summarized_verdict2(Rest,Old,New) ; New=fail). | |
38 | ||
39 | :- use_module(b_global_sets,[b_clear_global_set_type_definitions/0]). | |
40 | run_testcase(Filename,Testname,Type,Verdict) :- | |
41 | b_clear_global_set_type_definitions, | |
42 | catch(( absolute_file_name(Filename,AbsFilename), | |
43 | load_b_machine_as_term(AbsFilename,Machine,[]) -> | |
44 | ( run_testcase2(Type,Testname,Machine,Verdict) -> true | |
45 | ; Verdict = [verdict(Testname,*,error('run_testcase2 failed'))]) | |
46 | ; Verdict = [verdict(Testname,*,error('unable to load testfile'))]), | |
47 | X, | |
48 | Verdict = [verdict(Testname,*,error(X))]). | |
49 | ||
50 | run_testcase2(Type, Testname, complete_machine(Main, Machines, _), Verdict) :- | |
51 | ( extract_tests(Main,Machines,Test) -> | |
52 | ( \+ ground(Test) -> | |
53 | Verdict = [verdict(Testname,*,error('testcases not ground'))] | |
54 | ; check_machine(Main, Machines, Typed, Errors) -> | |
55 | ( run_testcase3(Type,Testname,Typed,Errors,Test,Verdict) -> true | |
56 | ; Verdict = [verdict(Testname,*,error('run_testcase3 failed'))]) | |
57 | ; | |
58 | Verdict = [verdict(Testname,*,fail('type checker failed'))]) | |
59 | ; | |
60 | Verdict = [verdict(Testname,*,error('extracting tests failed'))]). | |
61 | ||
62 | extract_tests(Main,Machines,Tests) :- | |
63 | findall(test(Name,T), | |
64 | ( get_secs(Main,Machines,Secs), | |
65 | member(definitions(_,Defs),Secs), | |
66 | member(expression_definition(_,Fullname,[],string(_,TestAtom)),Defs), | |
67 | atom_chars(Fullname,CFullname), | |
68 | append(['T','E','S','T','_'],CName,CFullname), | |
69 | atom_chars(Name,CName), | |
70 | atom_codes(TestAtom,TestCodes1),append(TestCodes1,[0'.],TestCodes), | |
71 | read_from_codes(TestCodes,T)), | |
72 | Tests). | |
73 | get_secs(Name,Machines,Secs) :- | |
74 | member(abstract_machine(_,_ModelType,machine_header(_,Name,_),Secs),Machines). | |
75 | get_secs(Name,Machines,Secs) :- | |
76 | member(refinement_machine(_,machine_header(_,Name,_),_Refines,Secs),Machines). | |
77 | ||
78 | ||
79 | run_testcase3(typesok, Testname, Typed, Errors, Tests, Verdict) :- | |
80 | ( Errors = [] -> | |
81 | Verdict = [verdict(Testname,typecheck,pass)|Verdict1], | |
82 | run_checks(Tests,Testname,Typed,Verdict1) | |
83 | ; | |
84 | Verdict = [verdict(Testname,*,fail('unexpected errors from type-checker', Errors))]). | |
85 | ||
86 | run_checks([],_,_,[]). | |
87 | run_checks([test(Name,Test)|Rest],Testname,Typed,[verdict(Testname,Name,Verdict)|VRest]) :- | |
88 | run_check(Test,Typed,Verdict), | |
89 | run_checks(Rest,Testname,Typed,VRest). | |
90 | ||
91 | run_check(ElemPos:ExpectedType, Typed, Verdict) :- | |
92 | ( slashes_to_list(ElemPos,ElemPosL), | |
93 | get_element(ElemPosL,Typed,Element) -> | |
94 | ( get_texpr_type(Element,Type) -> | |
95 | ( Type == ExpectedType -> | |
96 | Verdict = pass | |
97 | ; | |
98 | safe_pretty_type(ExpectedType, PExp), | |
99 | safe_pretty_type(Type, PType), | |
100 | ajoin(['expected ',PExp,', but was ', PType],Msg), | |
101 | Verdict = fail(Msg)) | |
102 | ; | |
103 | Verdict = fail('got ill-formed expression')) | |
104 | ; | |
105 | write_to_codes(ElemPos,ElemStr), | |
106 | atom_codes(ElemAtom,ElemStr), | |
107 | ajoin(['element ',ElemAtom,' not found'], Msg), | |
108 | Verdict = fail(Msg)). | |
109 | ||
110 | safe_pretty_type(Type,Text) :- | |
111 | (pretty_type(Type,Text) -> true ; Text = '<failed to pretty type>'). | |
112 | ||
113 | slashes_to_list(A/B,List) :- | |
114 | !,slashes_to_list(A,AList), | |
115 | slashes_to_list(B,BList), | |
116 | append(AList,BList,List). | |
117 | slashes_to_list(X,[X]). | |
118 | ||
119 | get_element([Section|Path],M,Elem) :- | |
120 | get_section(Section,M,Content), | |
121 | get_element2(Content,Path,Elem),!. | |
122 | get_element2([H|T],Path,Elem) :- !, | |
123 | member(Sub,[H|T]),get_element2(Sub,Path,Elem). | |
124 | get_element2(TExpr,Path,Elem) :- | |
125 | is_texpr(TExpr), | |
126 | get_texpr_expr(TExpr,Expr), | |
127 | ( Path = [] -> | |
128 | Elem=TExpr | |
129 | ; Expr = identifier(op(ID)) -> | |
130 | get_element3(Path,ID,TExpr,Elem) | |
131 | ; Expr = identifier(ID) -> | |
132 | get_element3(Path,ID,TExpr,Elem) | |
133 | ; Expr = operation(OpId,_,_,_),get_texpr_id(OpId,op(ID)) -> | |
134 | get_element3(Path,ID,TExpr,Elem) | |
135 | ; functor(Expr,Functor,_) -> | |
136 | get_element3(Path,Functor,TExpr,Elem)). | |
137 | get_element3([Path],Path,TExpr,TExpr). | |
138 | get_element3([Head|Rest],Head,TExpr,Elem) :- | |
139 | Rest=[_|_], | |
140 | syntaxtraversion(TExpr,_,_,_,Subs,_), | |
141 | get_element2(Subs,Rest,Elem). | |
142 | get_element3([*|Rest],Pattern,TExpr,Elem) :- | |
143 | Rest=[_|_],get_element3(Rest,Pattern,TExpr,Elem). | |
144 | get_element3([*|Rest],_Pattern,TExpr,Elem) :- | |
145 | Rest=[_|_], | |
146 | syntaxtraversion(TExpr,_,_,_,Subs,_), | |
147 | get_element2(Subs,[*|Rest],Elem). |