1 % (c) 2009-2013 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(b_abstract_interpreter, [
6 absint_check_boolean_expression/6,
7 absint_execute_statement/5,
8 absint_compute_expression/4,
9 find_abstract_transition/5
10 ]).
11
12 :- use_module(probsrc(module_information)).
13 :- module_info(group,plugin_absint).
14 :- module_info(description,'Abstract Interpreter for B.').
15 :- module_info(revision,'$Rev$').
16 :- module_info(lastchanged,'$LastChangedDate$').
17
18 :- use_module(library(samsort)).
19 :- use_module(library(lists)).
20
21 :- use_module(probsrc(error_manager)).
22 :- use_module(probsrc(bsyntaxtree)).
23 :- use_module(probsrc(b_interpreter)).
24 :- use_module(probsrc(store)).
25
26 :- use_module(b_abstract_mappings).
27 :- use_module(b_abstract_interpreter_helpers).
28
29 find_abstract_transition(Operation, StateBegin, StateTrans, Paras, Results) :-
30 execute_abstract_top_level_operation(Operation, _, StateBegin, StateTransInter, Paras, Results, Path),
31 Path \= precond(false),
32 StateTransInter = StateTrans.
33
34 execute_abstract_top_level_operation(Name,FullOperation,InState,NewState,Parameters,Results,Path) :-
35 b_interpreter:try_get_op_name(FullOperation, Name),
36 execute_abstract_operation(Name,FullOperation,InState,NewState,Parameters,Results,true,Path).
37
38 execute_abstract_operation(Name,Operation,InState,NewOutState,ParaValues,ResultValues,TopLevel,Path) :-
39 b_interpreter:b_get_machine_operation_for_animation(Name,Results,Parameters,Body,_OType,TopLevel),
40 execute_abstract_operation(Name,Operation,InState,NewOutState,Body,Parameters,ParaValues,Results,ResultValues,TopLevel,Path).
41
42 execute_abstract_operation(Name,RealFullOperation,InState,SortedStateFinish,Body,Parameters,ParameterValues,Results,ResultValues,TopLevel,Path) :-
43 absint_set_up_localstate(Parameters,ParameterValues,LocalState),
44 absint_set_up_undefined_localstate(Results,InState,NewInState),
45 (
46 TopLevel==true
47 -> absint_execute_top_level_statement(Body,LocalState,NewInState,Updates,Path)
48 ; absint_execute_statement(Body,LocalState,NewInState,Updates,Path)
49 ),
50 l_expand_and_normalise_values(ParameterValues,NormalisedParaValues,Parameters),
51 Operation =.. [Name|NormalisedParaValues],
52 (
53 Results == []
54 -> RealFullOperation = Operation
55 ; RealFullOperation = '-->'(Operation,ResultValues)
56 ),
57 state_store_list(Updates,NewInState,OutState),
58 absint_get_results(Results,OutState,ResultValues,StateFinish),
59 samsort(StateFinish,SortedStateFinish).
60
61 % checking of boolean expressions might modify the state!
62 absint_check_boolean_expression(b(Expr, _, _),LocalState,LocalStateOut,State,StateOut,Test) :-
63 absint_check_boolean_expression2(Expr,LocalState,LocalStateOut,State,StateOut,Test).
64
65 absint_check_boolean_expression2(truth,LS,LS,S,S,true) :- !.
66 absint_check_boolean_expression2(falsity,LS,LS,S,S,false) :- !.
67
68 absint_check_boolean_expression2(conjunct(Arg1,Arg2),LocalStateIn,LocalStateIn,StateIn,StateOut,Test) :-
69 !, absint_check_boolean_expression(Arg1,LocalStateIn,LocalStateIn,StateIn,TempStateOut,Result1),
70 absint_check_boolean_expression(Arg2,LocalStateIn,LocalStateIn,TempStateOut,StateOut,Result2),
71 (Result1 = Result2 -> Test = true ; Test = false).
72 absint_check_boolean_expression2(implication(Arg1,Arg2),LocalStateIn,LocalStateIn,StateIn,StateOut,Test) :-
73 !, absint_check_boolean_expression(Arg1,LocalStateIn,LocalStateIn,StateIn,TempStateOut,Result1),
74 absint_check_boolean_expression(Arg2,LocalStateIn,LocalStateIn,TempStateOut,StateOut,Result2),
75 (Result1 = true, Result2 = false -> Test = false ; Test = true).
76
77 absint_check_boolean_expression2(BinExpr,LocalStateIn,LocalStateIn,StateIn,StateOut,Test) :-
78 binary_operator(BinExpr, BOP, Arg1, Arg2), !,
79 absint_compute_expression(Arg1,LocalStateIn,StateIn,Arg1Val),
80 absint_compute_expression(Arg2,LocalStateIn,StateIn,Arg2Val),
81 call_binary_test(BOP,Arg1Val,Arg2Val,NewVal1,NewVal2,Test),
82 test_binary_update(Arg1, Arg2, NewVal1, NewVal2, StateIn, StateOut).
83
84 absint_check_boolean_expression2(Test,LocalState,_LocalStateOut,InState,_OutState,_) :-
85 !, add_error_fail(absint_check_boolean_expression2, 'Boolean Expression not implemented: ', [Test,LocalState,InState]).
86
87 % execution of statements
88 absint_execute_top_level_statement(TExpr,LocalState,InState,OutState,Path) :-
89 get_texpr_expr(TExpr,Stmt),
90 absint_execute_top_level_statement2(Stmt,TExpr,LocalState,InState,OutState,Path).
91 absint_execute_top_level_statement2(precondition(PreCond,Body),_,LocalState,InState,OutState,Path) :-
92 !, absint_check_boolean_expression(PreCond,LocalState,LocalStateOut,InState,TempState,true),
93 absint_execute_statement(Body,LocalStateOut,TempState,OutState,Path).
94 absint_execute_top_level_statement2(_,TExpr,LocalState,InState,OutState,Path) :-
95 absint_execute_statement(TExpr,LocalState,InState,OutState,Path).
96
97 absint_execute_statement(b(Stmt,_,Infos),LocalState,InState,OutState,Path) :-
98 absint_execute_statement2(Stmt,Infos,LocalState,InState,OutState,Path).
99
100 absint_execute_statement2(assign(VarExprs, ValExprs), _Infos,LocalState,InState,OutState,assign) :-
101 !, absint_compute_expressions(ValExprs, LocalState, InState, ValExprs2),
102 assign_vars(VarExprs, ValExprs2, LocalState, InState, NewVars, NewVals),
103 assign_vals_to_vars(NewVars, NewVals, StoreList),
104 OutState = StoreList.
105 absint_execute_statement2(assign_single_id(IDE,Expr),_Infos,LocalState,InState,OutState,assign) :-
106 get_texpr_id(IDE,ID),!,
107 absint_compute_expression(Expr,LocalState,InState,Value),
108 OutState = [bind(ID,Value)].
109 absint_execute_statement2(if(IfList),_Infos,LocalState,InState,OutState,if) :-
110 !, execute_else_list(IfList,LocalState,InState,OutState).
111 absint_execute_statement2(parallel(Statements),_Infos,LocalState,InState,OutState,parallel(Paths)) :-
112 !, execute_statements_in_parallel(Statements, LocalState, InState, OutState, Paths).
113 absint_execute_statement2(select(Whens),_Infos,LocalState,InState,OutState,select(Nr,Path)) :-
114 !, get_texpr_expr(TExpr,select_when(PreCond, Body)),
115 nth1(Nr, Whens, TExpr),
116 absint_check_boolean_expression(PreCond,LocalState,LocalStateOut,InState,NewInState,true),
117 absint_execute_statement(Body,LocalStateOut,NewInState,OutState,Path).
118 absint_execute_statement2(Stmt,_Infos,LocalState,InState,_OutState,_Path) :-
119 !, add_error_fail(absint_execute_statement2, 'Statement not implemented: ', [Stmt,LocalState,InState]).
120
121 % computation of expressions
122 absint_compute_expressions([], _, _, []).
123 absint_compute_expressions([EXPRsHd|EXPRsTl],LocalState,InState,[ValHd|ValTl]) :-
124 absint_compute_expression(EXPRsHd,LocalState,InState,ValHd),
125 absint_compute_expressions(EXPRsTl,LocalState,InState,ValTl).
126
127 absint_compute_expression(b(Expr,Type,Info),LocalState,StateIn,Val) :-
128 absint_compute_expression2(Expr,Type,Info,LocalState,StateIn,Val),!.
129
130 absint_compute_expression2(couple(Arg1,Arg2),_Type,_Info,LocalState,StateIn,couple(Arg1Val,Arg2Val)) :-
131 !, absint_compute_expression(Arg1,LocalState,StateIn,Arg1Val),
132 absint_compute_expression(Arg2,LocalState,StateIn,Arg2Val).
133 absint_compute_expression2(identifier(Key),_Type,_Info,LocalState,StateIn,Value) :-
134 !, state_lookup(Key,LocalState,StateIn,Value).
135 absint_compute_expression2(integer(IntVal),Type,Info,_LocalState,_StateIn,AbsVal) :-
136 !, call_alpha(integer(IntVal),Type,Info,AbsVal).
137 absint_compute_expression2(empty_set,Type,Info,_LocalState,_StateIn,AbsVal) :-
138 !, call_alpha(empty_set,Type,Info,AbsVal).
139 absint_compute_expression2(boolean_true,Type,Info,_LocalState,_StateIn,AbsVal) :-
140 !, call_alpha(boolean_true,Type,Info,AbsVal).
141 absint_compute_expression2(boolean_false,Type,Info,_LocalState,_StateIn,AbsVal) :-
142 !, call_alpha(boolean_false,Type,Info,AbsVal).
143
144 absint_compute_expression2(Expr,_Type,_Info,LocalState,StateIn,AbsVal) :-
145 unary_operator(Expr,OP,Arg), !,
146 absint_compute_expression(Arg,LocalState,StateIn,ArgVal),
147 call_unary_expression(OP,ArgVal,AbsVal).
148 absint_compute_expression2(Expr,_Type,_Info,LocalState,StateIn,AbsVal) :-
149 binary_operator(Expr,OP,Arg1,Arg2), !,
150 absint_compute_expression(Arg1,LocalState,StateIn,Arg1Val),
151 absint_compute_expression(Arg2,LocalState,StateIn,Arg2Val),
152 call_binary_expression(OP,Arg1Val,Arg2Val,AbsVal).
153 absint_compute_expression2(Expr,_Type,_Info,LocalState,StateIn,AbsVal) :-
154 nary_operator(Expr,OP,Args), !,
155 absint_compute_expressions(Args,LocalState,StateIn,ArgVals),
156 call_nary_expression(OP,ArgVals,AbsVal).
157
158 absint_compute_expression2(X,T,I,LS,S,_V) :-
159 !, add_error_fail(absint_compute_expression2, 'Expression not implemented: ', [X,T,I,LS,S]).