| 1 | % (c) 2009-2019 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_read_write_info,[get_accessed_vars/4, get_accessed_vars/5, | |
| 6 | recompute_while_read_write_info/2, | |
| 7 | get_nondet_modified_vars/3, | |
| 8 | tcltk_read_write_matrix/1, | |
| 9 | tcltk_variable_read_write_matrix/2, | |
| 10 | tcltk_dot_variable_modification_analysis/1, | |
| 11 | tcltk_get_guards_for_ops/1, | |
| 12 | tcltk_get_parameter_free_guards_for_ops/1, | |
| 13 | b_get_read_write/3, | |
| 14 | b_get_operation_read_guard_vars/3, | |
| 15 | b_get_read_write_vars/5, | |
| 16 | b_get_written_variables/1, check_all_variables_written/0, | |
| 17 | %,b_get_read_may_must_write/7 % currently not used outside | |
| 18 | ||
| 19 | get_lhs_assigned_identifier/2 | |
| 20 | ]). | |
| 21 | ||
| 22 | ||
| 23 | :- use_module(module_information,[module_info/2]). | |
| 24 | :- module_info(group,typechecker). | |
| 25 | :- module_info(description,'ProBs type checker and type inference module.'). | |
| 26 | ||
| 27 | :- use_module(library(lists)). | |
| 28 | :- use_module(library(ordsets)). | |
| 29 | :- use_module(self_check). | |
| 30 | :- use_module(error_manager). | |
| 31 | :- use_module(bsyntaxtree). | |
| 32 | ||
| 33 | ||
| 34 | recompute_while_read_write_info(TExpr,NewTExpr) :- | |
| 35 | (transform_bexpr(b_read_write_info:update_while_info,TExpr,NewTExpr) | |
| 36 | -> true | |
| 37 | ; add_internal_error('Call failed: ',transform_bexpr(b_read_write_info:update_while_info,TExpr,NewTExpr)), | |
| 38 | NewTExpr=TExpr). | |
| 39 | ||
| 40 | :- use_module(translate,[print_bexpr/1]). | |
| 41 | :- public update_while_info/2. | |
| 42 | update_while_info(b(WHILE,subst,OldInfo),b(WHILE,subst,NewInfo)) :- | |
| 43 | WHILE = while(_TPred,_TBody,_TInv,TVar), | |
| 44 | get_accessed_vars(b(WHILE,subst,OldInfo),[],Modifies,Reads), | |
| 45 | (debug:debug_mode(off) -> true | |
| 46 | ; nl,print('UPDATING WHILE with VARIANT: '),translate:print_bexpr(TVar),nl, | |
| 47 | format(' WHILE Reads : ~w~n Modifies : ~w~n',[Reads,Modifies]) | |
| 48 | ), | |
| 49 | (delete(OldInfo,reads(OldReads),OI1) -> true ; OldReads=[], OI1=OldInfo), | |
| 50 | (delete(OI1,modifies(OldModifies),OI2) -> true ; OldModifies=[], OI2=OI1), | |
| 51 | ((Reads,Modifies)=(OldReads,OldModifies) | |
| 52 | -> NewInfo=OldInfo | |
| 53 | ; format('***** different from Reads : ~w~n Modifies : ~w~n',[OldReads,OldModifies]), | |
| 54 | ord_subtract(Reads,OldReads,NewR), | |
| 55 | ord_subtract(OldReads,Reads,DelR), | |
| 56 | format(' added: ~w~n deleted: ~w~n****~n',[NewR,DelR]), | |
| 57 | NewInfo = [modifies(Modifies),reads(Reads)|OI2] | |
| 58 | ). | |
| 59 | ||
| 60 | % TO DO: also update info for operation call ! | |
| 61 | ||
| 62 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 63 | ||
| 64 | :- use_module(bsyntaxtree,[get_global_identifiers/1]). | |
| 65 | ||
| 66 | /* get_accessed_vars/4 computes the variables that are read or written to | |
| 67 | by a substitution. | |
| 68 | get_accessed_vars(+Subst,+LocalVars,-Modified,-Reads): | |
| 69 | Subst is the substitution (as a typed syntax tree) | |
| 70 | LocalVars is a list of (untyped) ids that are local variables. | |
| 71 | Local variables are ignored and not included in the list of read or written | |
| 72 | variables. | |
| 73 | Modified is the list of (untyped) identifiers that are written by the substitution and | |
| 74 | Reads is the list of (untyped) identifiers that are read. */ | |
| 75 | get_accessed_vars(TSubst,LocalVars,Modified,Reads) :- | |
| 76 | get_accessed_vars(TSubst,LocalVars,Modified,_,Reads). | |
| 77 | get_accessed_vars(TSubst,LocalVars,Modified,NonDetModified,Reads) :- | |
| 78 | get_global_identifiers(IS), % TO DO: currently this information is set up only *after* type checking !! | |
| 79 | % this means the accessed vars will also contain SETS and enumerated set elements ! | |
| 80 | % either we need to filter them out later, or change the startup / precompilation process | |
| 81 | list_to_ord_set(LocalVars,SLV), | |
| 82 | ord_union(IS,SLV,LocalVarsToIgnore), | |
| 83 | get_accessed_vars1(TSubst,LocalVarsToIgnore,In,Out), | |
| 84 | extract_reads_and_modifies(In,Out,Modified,NonDetModified,Reads). | |
| 85 | extract_reads_and_modifies(mrinfo(UnsortedMods,NonDetMods,UnsortedReads),mrinfo([],[],[]), | |
| 86 | Modified,NonDetModified,Reads) :- | |
| 87 | sort(UnsortedMods,Modified), | |
| 88 | sort(NonDetMods,NonDetModified), | |
| 89 | sort(UnsortedReads,Reads). | |
| 90 | ||
| 91 | % get variables which are modified non-deterministically; does not traverse operation calls at the moment | |
| 92 | get_nondet_modified_vars(TSubst,LocalVars,NonDetModified) :- | |
| 93 | Out=mrinfo([],[],[]), | |
| 94 | list_to_ord_set(LocalVars,SLocalVars), | |
| 95 | get_accessed_vars1(TSubst,SLocalVars,In,Out), | |
| 96 | In=mrinfo(_,UnsortedMods,_), | |
| 97 | sort(UnsortedMods,NonDetModified). | |
| 98 | ||
| 99 | ||
| 100 | is_operation_call(operation_call(Operation,Results,Arguments),Operation,Results,Arguments). | |
| 101 | is_operation_call(operation_call_in_expr(Operation,Arguments),Operation,[],Arguments). | |
| 102 | ||
| 103 | get_accessed_vars1(TSubst,LocalVars,In,Out) :- | |
| 104 | get_texpr_expr(TSubst,Subst), | |
| 105 | ( is_operation_call(Subst,Operation,Results,Arguments) -> | |
| 106 | get_texpr_info(TSubst,Info), | |
| 107 | def_get_texpr_id(Operation,op(OperationName)), %print(info(OperationName,Info)),nl, | |
| 108 | memberchk(modifies(MVars),Info), | |
| 109 | (memberchk(non_det_modifies(NonDetMVars),Info) -> true ; NonDetMVars=[]), | |
| 110 | memberchk(reads(RVars),Info), | |
| 111 | % info fields added in btype2(operation(...) in btypechecker.pl | |
| 112 | %op_modifies_reads_cache(OperationName,MVarsC,RVarsC) %this is no longer necessary | |
| 113 | (ground(MVars),ground(RVars) | |
| 114 | -> true | |
| 115 | ; add_error(b_read_write_info, 'Cannot obtain modifies/reads info for called operation (probably illegal local call): ',OperationName), | |
| 116 | % TEST 655 used to reach this branch | |
| 117 | MVars=[], RVars=[], NonDetMVars=[] | |
| 118 | % this should only happen when local operation called !?! | |
| 119 | % or ensure that operations are processed before we reach operation calls | |
| 120 | % this may be problematic for local operations | |
| 121 | ), | |
| 122 | % print(compute_acc_vars_for_op_call(modifies(MVars,NonDetMVars),Info,Subst)),nl, %trace, | |
| 123 | accessed_vars_for_operation_call(MVars,NonDetMVars,RVars,LocalVars,Results,Arguments,In,Out) | |
| 124 | ; get_accessed_vars2(Subst,LocalVars,In,Out) -> | |
| 125 | true | |
| 126 | ; Subst = identifier(ID) -> add_error(b_read_write_info,'Identifier not a valid B Operation: ',ID,TSubst),In=Out | |
| 127 | ; otherwise -> | |
| 128 | add_internal_error('Could not extract information about accessed variables for substitution', | |
| 129 | get_accessed_vars2(Subst,LocalVars,In,Out)), | |
| 130 | %trace, get_accessed_vars2(Subst,LocalVars,In,Out), | |
| 131 | fail). | |
| 132 | accessed_vars_for_operation_call(MVars,NonDetMVars,RVars,LocalVars,Results,Arguments) --> | |
| 133 | add_non_local_modified_vars(MVars,LocalVars), | |
| 134 | add_non_local_read_vars(RVars,LocalVars), | |
| 135 | add_modified_vars(Results,LocalVars), | |
| 136 | add_non_local_non_det_modified_vars(NonDetMVars,LocalVars), | |
| 137 | add_read_vars_l(Arguments,LocalVars). | |
| 138 | ||
| 139 | get_accessed_vars2(skip,_) --> !. | |
| 140 | get_accessed_vars2(block(Subst),LocalVars) --> get_accessed_vars1(Subst,LocalVars). | |
| 141 | get_accessed_vars2(init_statement(Subst),LocalVars) --> get_accessed_vars1(Subst,LocalVars). | |
| 142 | get_accessed_vars2(assertion(A,Subst),R) --> add_read_vars(A,R),get_accessed_vars1(Subst,R). | |
| 143 | get_accessed_vars2(assign(LHS,E),R) --> %Note: LHS can be nested function application f(a)(b) := | |
| 144 | {maplist(get_lhs_assigned_identifier,LHS,Ids)}, add_modified_vars(Ids,R), | |
| 145 | {convlist(get_lhs_read_expression,LHS,LHS_R), append(LHS_R,E,RE)}, add_read_vars_l(RE,R). | |
| 146 | get_accessed_vars2(assign_single_id(Id,E),R) --> | |
| 147 | add_read_vars_l([E],R), % Note: LHS is a single Identifier: nothing is ever read there | |
| 148 | add_modified_vars([Id],R). | |
| 149 | get_accessed_vars2(precondition(P,Subst),R) -->add_read_vars(P,R),get_accessed_vars1(Subst,R). | |
| 150 | get_accessed_vars2(assertion(Subst),R) --> get_accessed_vars1(Subst,R). | |
| 151 | get_accessed_vars2(choice(Substs),R) --> get_accessed_vars_for_choice(Substs,R). | |
| 152 | get_accessed_vars2(if(Substs),R) --> get_accessed_vars_for_if(Substs,R). | |
| 153 | get_accessed_vars2(select(Whens,Else),R) --> get_accessed_vars_for_select(Whens,Else,R). | |
| 154 | get_accessed_vars2(select(Whens),R) --> get_accessed_vars_for_select(Whens,none,R). | |
| 155 | get_accessed_vars2(case(Expr,Substs,Else),R) --> get_accessed_vars_for_case(Expr,Substs,Else,R). | |
| 156 | get_accessed_vars2(case_or(Exprs,Subst),R) --> add_read_vars_l(Exprs,R),get_accessed_vars1(Subst,R). | |
| 157 | get_accessed_vars2(any(Ids,G,Subst),R) --> get_mrinfo(ModIn,_,_), | |
| 158 | add_tvars_to_ord_list(R,Ids,L),add_read_vars(G,L), | |
| 159 | get_accessed_vars1(Subst,L), | |
| 160 | add_delta_modified_to_non_det_modified(ModIn). | |
| 161 | get_accessed_vars2(let(Ids,G,Subst),R) --> | |
| 162 | add_tvars_to_ord_list(R,Ids,L),add_read_vars(G,L),get_accessed_vars1(Subst,L). | |
| 163 | get_accessed_vars2(lazy_let_subst(ID,SharedExpr,Subst),R) --> add_tvars_to_ord_list(R,[ID],L), | |
| 164 | add_read_vars(SharedExpr,L),get_accessed_vars1(Subst,L). | |
| 165 | get_accessed_vars2(becomes_element_of(Ids,E),R) --> add_non_det_modified_vars(Ids,R),add_read_vars(E,R). | |
| 166 | get_accessed_vars2(becomes_such(Ids,E),LocalVars0) --> add_non_det_modified_vars(Ids,LocalVars0), | |
| 167 | {append_primed_vars(Ids,LocalVars0,LocalVars1)}, % all Ids are already marked as accessed, any reference to Id$0 is a read of the old value; do not add Id$0 to the accessed variables | |
| 168 | add_read_vars(E,LocalVars1). | |
| 169 | %get_accessed_vars2(evb2_becomes_such(Ids,E),R) --> % now translated to becomes_such | |
| 170 | % add_non_det_modified_vars(Ids,R), add_read_vars(E,R). | |
| 171 | get_accessed_vars2(sequence(Substs),R) --> get_accessed_vars_l(Substs,R). | |
| 172 | get_accessed_vars2(parallel(Substs),R) --> get_accessed_vars_l(Substs,R). | |
| 173 | get_accessed_vars2(while(Cond,Subst,Inv,Variant),R) --> | |
| 174 | get_accessed_vars_for_while(Cond,Subst,Inv,Variant,R). | |
| 175 | get_accessed_vars2(var(Ids,Subst),R) --> add_tvars_to_ord_list(R,Ids,L),get_accessed_vars1(Subst,L). | |
| 176 | % TODO: we need information about which variables are modified by an external function | |
| 177 | get_accessed_vars2(external_subst_call(_Name,Exprs),R) --> add_read_vars_l(Exprs,R). | |
| 178 | get_accessed_vars2(rlevent(_Name,_Section,_Status,Params,Guard,Theorems,Actions,VWitnesses,PWitnesses,_Unmod,AbstractEvents),R) --> | |
| 179 | add_tvars_to_ord_list(R,Params,L), | |
| 180 | add_read_vars(Guard,L), | |
| 181 | add_read_vars_l(Theorems,L), | |
| 182 | add_witness_read_vars_l(VWitnesses,L), | |
| 183 | add_witness_read_vars_l(PWitnesses,L), | |
| 184 | get_accessed_vars_l(Actions,L), | |
| 185 | get_accessed_vars_l(AbstractEvents,L). | |
| 186 | ||
| 187 | get_accessed_vars_for_while(Cond,Subst,Inv,Variant,Locals) --> | |
| 188 | get_accessed_vars_for_while2(Inv,Locals), | |
| 189 | add_read_vars(Cond,Locals), | |
| 190 | add_read_vars(Variant,Locals), | |
| 191 | get_accessed_vars1(Subst,Locals). | |
| 192 | get_accessed_vars_for_while2(Inv,Locals,In,Out) :- | |
| 193 | add_read_vars(Inv,Locals,LI,LO), | |
| 194 | extract_reads_and_modifies(LI,LO,Modified,_,Reads0), | |
| 195 | maplist(remove_optional_prime,Reads0,Reads), | |
| 196 | list_to_ord_set(Reads,SReads), % removing prime can create duplicates | |
| 197 | add_non_local_read_vars(SReads,Locals,In,Inter), | |
| 198 | add_non_local_modified_vars(Modified,Locals,Inter,Out). | |
| 199 | remove_optional_prime(Id,Orig) :- atom_concat(Orig,'$0',Id),!. | |
| 200 | remove_optional_prime(Id,Id). | |
| 201 | ||
| 202 | get_accessed_vars_for_if(ElseIfs,Locals) --> | |
| 203 | { maplist(split_elseif,ElseIfs,Conds,Subst), | |
| 204 | ( if_has_else_block(Conds) -> HasElse = has_else | |
| 205 | ; otherwise -> HasElse = if_with_no_else) }, | |
| 206 | % mark all used variables in the conditions as read | |
| 207 | add_read_vars_l(Conds,Locals), | |
| 208 | get_accessed_vars_for_if_when(HasElse,Subst,Locals). | |
| 209 | split_elseif(Expr,Cond,Subst) :- get_texpr_expr(Expr,if_elsif(Cond,Subst)). | |
| 210 | ||
| 211 | get_accessed_vars_for_select(Whens,Else,Locals) --> | |
| 212 | { maplist(split_when,Whens,Conds,Subst1), | |
| 213 | ( Else = none -> | |
| 214 | HasElse=select_no_else, Subst = Subst1 | |
| 215 | ; otherwise -> | |
| 216 | HasElse=has_else, Subst = [Else|Subst1]) }, | |
| 217 | % mark all used variables in the conditions as read | |
| 218 | add_read_vars_l(Conds,Locals), | |
| 219 | get_accessed_vars_for_if_when(HasElse,Subst,Locals). | |
| 220 | split_when(Expr,Cond,Subst) :- get_texpr_expr(Expr,select_when(Cond,Subst)). | |
| 221 | ||
| 222 | get_accessed_vars_for_if_when(HasElse,Subst,Locals) --> | |
| 223 | { get_accessed_vars_for_if_when2(HasElse,Subst,Locals,Modified,NonDetModifies,Reads) }, | |
| 224 | add_read_vars2(Reads), | |
| 225 | %add_modified_vars2(Modified) | |
| 226 | ? | ({(HasElse==has_else ; HasElse==if_with_no_else ; Subst = [_,_|_])} |
| 227 | -> {ord_union(NonDetModifies,Modified,M2)}, | |
| 228 | add_non_det_modified_vars2(M2) | |
| 229 | ; add_non_det_modified_vars2(NonDetModifies), | |
| 230 | add_modified_vars2(Modified) % there is only one branch: Modified variables not also marked as non-det modified | |
| 231 | ). | |
| 232 | ||
| 233 | :- meta_predicate maplist5(4,-,-,-,-). | |
| 234 | maplist5(_P,[],[],[],[]). | |
| 235 | maplist5(P,[H1|T1],[H2|T2],[H3|T3],[H4|T4]) :- | |
| 236 | if(call(P,H1,H2,H3,H4), | |
| 237 | maplist5(P,T1,T2,T3,T4), | |
| 238 | (add_internal_error('Call fails: ',maplist5(P,H1,H2,H3,H4)), | |
| 239 | fail)). | |
| 240 | ||
| 241 | get_accessed_vars_for_if_when2(has_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome) :- | |
| 242 | maplist5(get_accessed_vars_x(Locals),Subst,Modifies,NonDetModifies,Reads), | |
| 243 | % We want to calculate those elements that are modified by some (in the union) | |
| 244 | % but not by all (in the intersection) | |
| 245 | ord_union(NonDetModifies,NonDetModifiedBySome), | |
| 246 | ord_union(Modifies,ModifiedBySome), | |
| 247 | ord_intersection(Modifies,ModifiedByAll), | |
| 248 | ord_subtract(ModifiedBySome,ModifiedByAll,ModifiedByNotAll), | |
| 249 | % we add those values that are not modified by all to the set of read variables | |
| 250 | % because e.g. "IF P THEN x:=1 END" is equivalent to "IF P THEN x:=1 ELSE x:=x END" | |
| 251 | ord_union([ModifiedByNotAll|Reads],ReadBySome). | |
| 252 | get_accessed_vars_for_if_when2(select_no_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome) :- | |
| 253 | % Note "SELECT P THEN x:=1 END" is NOT equivalent to "SELECT P THEN x:=1 ELSE x:=x END" ! | |
| 254 | % But treatment for computing ModiiedBySome,ReadBySome is identical | |
| 255 | get_accessed_vars_for_if_when2(if_with_no_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome). | |
| 256 | get_accessed_vars_for_if_when2(if_with_no_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome) :- | |
| 257 | % no else block present, we must assume that each written variable | |
| 258 | % can also be treated like a read variable (see example in the other condition) | |
| 259 | maplist5(get_accessed_vars_x(Locals),Subst,Modifies,NonDetModifies,Reads), | |
| 260 | ord_union(NonDetModifies,NonDetModifiedBySome), | |
| 261 | ord_union(Modifies,ModifiedBySome), | |
| 262 | ord_union([ModifiedBySome|Reads],ReadBySome). | |
| 263 | ||
| 264 | get_accessed_vars_for_choice(Substs,Locals,In,mrinfo(ModOut,NDOut2,Read)) :- | |
| 265 | get_accessed_vars_for_if_when(has_else,Substs,Locals,In,Out), | |
| 266 | In = mrinfo(ModIn,_,_), | |
| 267 | Out = mrinfo(ModOut,NDOut,Read), % these three fields will be all variables | |
| 268 | % mark all assignments as non-deterministically chosen: | |
| 269 | add_modified_to_non_det_modified(ModIn,ModOut,NDOut,NDOut2). | |
| 270 | ||
| 271 | add_modified_to_non_det_modified(ModIn,ModOut,NDIn,NDOut) :- ModIn==ModOut,!,NDIn=NDOut. | |
| 272 | add_modified_to_non_det_modified([H|ModIn],ModOut,[H|NDIn],NDOut) :- | |
| 273 | add_modified_to_non_det_modified(ModIn,ModOut,NDIn,NDOut). % duplicates in NDOut not an issue !?! | |
| 274 | ||
| 275 | get_mrinfo(Modified,NonDetModified,InRead,I,I) :- | |
| 276 | I = mrinfo(Modified,NonDetModified,InRead). | |
| 277 | ||
| 278 | add_delta_modified_to_non_det_modified(ModIn,mrinfo(ModOut,NonDet,Read),mrinfo(ModOut,NonDet2,Read)) :- | |
| 279 | add_modified_to_non_det_modified(ModIn,ModOut,NonDet,NonDet2). | |
| 280 | ||
| 281 | get_accessed_vars_for_case(Expr,Eithers,Else,Locals) --> | |
| 282 | % we can treat a case statement analogously to an IF-THEN-ELSE statement | |
| 283 | % where an ELSE is present | |
| 284 | % additionally, we have to add all expressions to the read set | |
| 285 | add_read_vars(Expr,Locals), | |
| 286 | { maplist(split_case_or,Eithers,ExprsList,Substs), append(ExprsList,Exprs) }, | |
| 287 | add_read_vars_l(Exprs,Locals), | |
| 288 | get_accessed_vars_for_if_when(has_else,[Else|Substs],Locals). | |
| 289 | split_case_or(CaseOr,Exprs,Subst) :- get_texpr_expr(CaseOr,case_or(Exprs,Subst)). | |
| 290 | ||
| 291 | % just the same as get_accessed_vars, but with different order of parameters | |
| 292 | % to allow call with maplist | |
| 293 | get_accessed_vars_x(Locals,Subst,Modifies,NonDetModifies,Reads) :- | |
| 294 | get_accessed_vars(Subst,Locals,Modifies,NonDetModifies,Reads). | |
| 295 | ||
| 296 | if_has_else_block(Conds) :- | |
| 297 | last(Conds,Cond),is_truth(Cond). | |
| 298 | ||
| 299 | % add ids of unsorted list of typed identifiers to sorted list of ids: | |
| 300 | add_tvars_to_ord_list(SortedVars,TIds,NewVars,X,X) :- | |
| 301 | get_texpr_ids(TIds,Ids), | |
| 302 | list_to_ord_set(Ids,SIds), | |
| 303 | ord_union(SortedVars,SIds,NewVars). | |
| 304 | %append(Vars,Ids,NewVars). | |
| 305 | ||
| 306 | add_read_vars_l([],_LocalVars) --> !. | |
| 307 | add_read_vars_l([Expr|Rest],LocalVars) --> !, | |
| 308 | add_read_vars(Expr,LocalVars), | |
| 309 | add_read_vars_l(Rest,LocalVars). | |
| 310 | add_read_vars_l(E,LV) --> !, {add_internal_error('Not a list: ',add_read_vars_l(E,LV,_,_))}. | |
| 311 | ||
| 312 | add_witness_read_vars_l([],_LocalVars) --> !. | |
| 313 | add_witness_read_vars_l([Expr|Rest],LocalVars) --> | |
| 314 | add_witness_read_vars(Expr,LocalVars), !, | |
| 315 | add_witness_read_vars_l(Rest,LocalVars). | |
| 316 | add_witness_read_vars_l(E,LV) --> !, {add_internal_error('Not a witness list: ',add_witness_read_vars_l(E,LV,_,_))}. | |
| 317 | ||
| 318 | % extract modified identifier from LHS of assign: | |
| 319 | get_lhs_assigned_identifier(b(function(LHS,_),_,_),Res) :- !, get_lhs_assigned_identifier(LHS,Res). | |
| 320 | get_lhs_assigned_identifier(ID,ID). | |
| 321 | ||
| 322 | % extract part of LHS of assign which reads information: | |
| 323 | get_lhs_read_expression(b(function(LHS,Read1),T,I),Res) :- !, | |
| 324 | Res = b(function(LHS,Read1),T,I). | |
| 325 | % old version which for f(a) := b only marked a as read in LHS f(a); now we also mark f | |
| 326 | % indeed f(a) := b is equivalent to f := f <+ {a|->b} ; so the old value of f is implicitly read (important for ltsmin symbolic model checking) | |
| 327 | %get_lhs_read_expression(b(function(LHS,Read1),_,_),Res) :- !, | |
| 328 | % (get_lhs_read_expression(LHS,Read2) -> create_couple(Read1,Read2,Res) | |
| 329 | % ; Res = Read1). | |
| 330 | ||
| 331 | add_witness_read_vars(b(witness(ID,Predicate),witness,_),LocalVars) --> !, | |
| 332 | % a parameter witness talks about a parameter no longer there: it is not really read here, but the predicate is used to set the any local parameter in another context | |
| 333 | % a variable witness alks about a variable non-deterministically assigned in the abstraction; we also pretend it is not read here (but assigned somewhere else) | |
| 334 | add_tvars_to_ord_list(LocalVars,[ID],LocalVars2), % we add ID to local variables not read "really" read here | |
| 335 | %{print(witness_add_read_vars(ID)),nl}, | |
| 336 | add_read_vars(Predicate,LocalVars2). | |
| 337 | ||
| 338 | add_read_vars(Expression,LocalVars) --> | |
| 339 | {find_identifier_uses(Expression,LocalVars,ReadVars)}, | |
| 340 | add_read_vars2(ReadVars). | |
| 341 | add_read_vars2(Vars,mrinfo(Modified,NonDetModified,InRead), | |
| 342 | mrinfo(Modified,NonDetModified,OutRead)) :- append(Vars,OutRead,InRead). | |
| 343 | ||
| 344 | add_non_local_read_vars(ReadVars,LocalVars) --> | |
| 345 | {ord_subtract(ReadVars,LocalVars,AddVars)}, | |
| 346 | add_read_vars2(AddVars). | |
| 347 | add_non_local_modified_vars(WriteVars,LocalVars) --> | |
| 348 | {ord_subtract(WriteVars,LocalVars,AddVars)}, | |
| 349 | add_modified_vars2(AddVars). | |
| 350 | ||
| 351 | add_modified_vars(Ids,LocalVars) --> | |
| 352 | {filter_result_vars(Ids,LocalVars,ModifiedVars)}, | |
| 353 | add_modified_vars2(ModifiedVars). | |
| 354 | add_modified_vars2(Vars,In,Res) :- | |
| 355 | (var(Vars) | |
| 356 | -> add_internal_error('Modified Vars variable: ',add_modified_vars2(Vars,In,Res)) | |
| 357 | ; true), | |
| 358 | In = mrinfo(InModified,NonDetModified,Read), | |
| 359 | Res = mrinfo(OutModified,NonDetModified,Read), | |
| 360 | append(Vars,OutModified,InModified). | |
| 361 | ||
| 362 | add_non_local_non_det_modified_vars(WriteVars,LocalVars) --> | |
| 363 | {ord_subtract(WriteVars,LocalVars,AddVars)}, | |
| 364 | add_non_det_modified_vars2(AddVars). | |
| 365 | ||
| 366 | add_non_det_modified_vars(Ids,LocalVars) --> | |
| 367 | {filter_result_vars(Ids,LocalVars,ModifiedVars)}, | |
| 368 | add_non_det_modified_vars2(ModifiedVars). | |
| 369 | add_non_det_modified_vars2(Vars,In,Res) :- | |
| 370 | (var(Vars) | |
| 371 | -> add_internal_error('Modified Vars variable: ',add_non_det_modified_vars2(Vars,In,Res)) | |
| 372 | ; true), | |
| 373 | In = mrinfo(InModified,InNonDetModified,Read), | |
| 374 | Res = mrinfo(OutModified,OutNonDetModified,Read), | |
| 375 | append(Vars,OutModified,InModified), | |
| 376 | append(Vars,OutNonDetModified,InNonDetModified). | |
| 377 | ||
| 378 | ||
| 379 | :- use_module(tools,[remove_all/3]). | |
| 380 | filter_result_vars(Ids,LocalVars,ModifiedVars) :- | |
| 381 | % extract_changed_id might fail if the user entered | |
| 382 | % a wrong LHS of an assignment. This should lead to an | |
| 383 | % type error, handled by the assign type checking rule. | |
| 384 | convlist(extract_changed_id,Ids,Names), | |
| 385 | remove_all(Names,LocalVars,ModifiedVars). | |
| 386 | extract_changed_id(Id,Name) :- | |
| 387 | get_texpr_id(Id,Name),!. | |
| 388 | extract_changed_id(Func,Name) :- | |
| 389 | get_texpr_expr(Func,function(TId,_)), !, | |
| 390 | extract_changed_id(TId,Name). % we can have nested function calls f(x)(y) := z | |
| 391 | extract_changed_id(X,Name) :- | |
| 392 | add_internal_error('Could not extract changed id: ',extract_changed_id(X,Name)),fail. | |
| 393 | ||
| 394 | get_accessed_vars_l([],_) --> []. | |
| 395 | get_accessed_vars_l([S|Rest],R) --> get_accessed_vars1(S,R),get_accessed_vars_l(Rest,R). | |
| 396 | ||
| 397 | ||
| 398 | ||
| 399 | :- use_module(tools,[number_suffix/3]). | |
| 400 | :- assert_must_succeed(( b_read_write_info:append_primed_vars([b(identifier(x),integer,[])],[],R), R = ['x$0'])). | |
| 401 | append_primed_vars(TIds,R,L) :- | |
| 402 | maplist(add_dollar_zero,TIds,Primed), | |
| 403 | append(Primed,R,L). | |
| 404 | :- assert_must_succeed(( b_read_write_info:add_dollar_zero(b(identifier(x),integer,[]),R), R = 'x$0')). | |
| 405 | add_dollar_zero(TId,P) :- | |
| 406 | get_texpr_id(TId,Id), | |
| 407 | number_suffix(Id,0,P). | |
| 408 | ||
| 409 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 410 | ||
| 411 | % READ-WRITE-INFO for OPERATIONS | |
| 412 | ||
| 413 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 414 | ||
| 415 | ||
| 416 | :- use_module(bmachine,[b_get_operation_normalized_read_write_info/3, b_get_machine_operation/4, | |
| 417 | b_get_machine_variables/1, b_get_machine_constants/1, b_is_variable/1]). | |
| 418 | ||
| 419 | b_get_read_write(O,R,W) :- | |
| 420 | if(b_get_operation_normalized_read_write_info(O,R,W),true, | |
| 421 | (R,W)=('$all','$all')). % it used to be that in Event-B no read information was stored; all calls to b_get_operation_normalized_read_write_info failed; has been fixed | |
| 422 | ||
| 423 | b_get_machine_operation_with_local_paras(OpName,AllLocalParas,Body) :- | |
| 424 | b_get_machine_operation(OpName,Results,Parameters,Body), | |
| 425 | append(Parameters,Results,TP), | |
| 426 | get_texpr_ids(TP,TPIds), | |
| 427 | list_to_ord_set(TPIds,AllLocalParas). | |
| 428 | ||
| 429 | /* We distinguish between read variables in the guard and read variables in the event statement */ | |
| 430 | b_get_read_write_guard_action(Operation,ReadGuard,ReadAction,Read,Write) :- | |
| 431 | b_get_read_write(Operation,Read,Write), | |
| 432 | b_get_operation_read_guard_vars(Operation,false,ReadGuard), | |
| 433 | b_get_machine_operation_with_local_paras(Operation,LocalParas,Body), | |
| 434 | get_texpr_expr(Body,RLEVENT), | |
| 435 | (RLEVENT = rlevent(_Name,_Section,_Stat,_Parameters,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_AbsEvents) -> | |
| 436 | % special code to deal with *all* guards/actions (also in abstractions) + not extract guards from actions | |
| 437 | % TO DO: maybe move this to get_guard/get_action (see below) ; or maybe provide parameter to choose | |
| 438 | % in some circumstances (Deadlock checking) it is sufficient to look at lowest refinement level | |
| 439 | % for LTSMin,... : we need info from all refinement levels and from theorems | |
| 440 | findall(A1,(get_full_eventb_action(RLEVENT,AA),member(A1,AA)),A) | |
| 441 | ; get_action(Operation,A) -> true | |
| 442 | ; otherwise -> add_error(b_get_read_write_guard_action,'Could not get action for operation: ',Operation), fail | |
| 443 | ), | |
| 444 | (is_list(A) % in case of Event-B events the action block is a list of assignments | |
| 445 | -> find_identifier_uses_l(A,LocalParas,RActionVars) % TO DO: use get_accessed_vars ? | |
| 446 | ; get_accessed_vars(A,LocalParas,_,RActionVars) | |
| 447 | ), | |
| 448 | list_to_ord_set(RActionVars,RActionVars1), | |
| 449 | rw_ord_intersection(RActionVars1,Read,ReadAction). | |
| 450 | %,debug_println(9,b_get_read_write(O,RGuard,R,W)). | |
| 451 | ||
| 452 | % this gets the variables/identifiers read in the guard of an operation | |
| 453 | % Note: this part will include parts of the guard that depend on the parameters | |
| 454 | b_get_operation_read_guard_vars(Operation,JustVariables,Result) :- | |
| 455 | b_get_machine_operation_with_local_paras(Operation,Paras,_), | |
| 456 | get_operation_guard(Operation,G), | |
| 457 | % RGuardVars can comprise also local variables by operations with parameters | |
| 458 | find_identifier_uses(G,Paras,RGuardVars), | |
| 459 | list_to_ord_set(RGuardVars,ReadGuard), | |
| 460 | (JustVariables=false | |
| 461 | -> Result = ReadGuard | |
| 462 | ; b_get_machine_variables(TVars),get_texpr_ids(TVars,Vars), | |
| 463 | list_to_ord_set(Vars,Variables), | |
| 464 | ord_intersection(ReadGuard,Variables,Result) | |
| 465 | ). | |
| 466 | ||
| 467 | % show full guards | |
| 468 | tcltk_get_guards_for_ops(list(Res)) :- | |
| 469 | findall([Name,' GUARD ',GS], | |
| 470 | (get_operation_guard(Name,G), | |
| 471 | translate:translate_bexpression(G,GS)), Res). | |
| 472 | ||
| 473 | % show guards which do not depend on parameters and the rest (the Action) | |
| 474 | tcltk_get_parameter_free_guards_for_ops(list(Res)) :- | |
| 475 | findall([Name,' LTSMIN-GUARD ',GS, 'ACTION ',AS], | |
| 476 | (get_operation_propositional_guards(Name,Guards,A),conjunct_predicates(Guards,G), | |
| 477 | translate:translate_bexpression(G,GS), | |
| 478 | translate:translate_substitution(A,AS)), Res). | |
| 479 | ||
| 480 | get_operation_guard(Operation,G) :- | |
| 481 | b_get_machine_operation(Operation,_RR,_P,TBody), | |
| 482 | get_texpr_expr(TBody,Body), | |
| 483 | get_operation_guard_aux(Body,Operation,G). | |
| 484 | ||
| 485 | :- use_module(probsrc(b_state_model_check), [get_guard/2]). | |
| 486 | get_operation_guard_aux(RLEVENT,_,G) :- | |
| 487 | RLEVENT = rlevent(_Name,_Section,_Stat,_Parameters,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_AbsEvents), | |
| 488 | !, | |
| 489 | findall(G1,get_full_eventb_guard(RLEVENT,G1),Gs), | |
| 490 | conjunct_predicates(Gs,G). | |
| 491 | get_operation_guard_aux(_,Operation,G) :- get_guard(Operation,G). | |
| 492 | ||
| 493 | ||
| 494 | % TO DO: we should move this code to b_state_model_check/predicate_debugger:get_operation_enabling_condition2 ? | |
| 495 | get_full_eventb_guard(rlevent(_Name,_Section,_Stat,_Parameters,Grd,Thms,_Act,_VWit,_PWit,_Unmod,AbsEvents),G) :- | |
| 496 | (G=Grd | |
| 497 | ; member(G,Thms) % this is relevant for LTS Min; but not for normal enabling analysis | |
| 498 | ; member(b(E,_,_),AbsEvents),get_full_eventb_guard(E,G)). | |
| 499 | get_full_eventb_action(rlevent(_Name,_Section,_Stat,_Parameters,_Grd,_Thm,Act,_VWit,_PWit,_Unmod,AbsEvents),A) :- | |
| 500 | (A=Act ; member(b(E,_,_),AbsEvents),get_full_eventb_action(E,A)). | |
| 501 | ||
| 502 | ||
| 503 | % Note: this is the LTSMin meaning of action (for LTSMin a guard depending on the parameter is part of the action) | |
| 504 | % Action will also contain parts of the guard that depend on parameters ! | |
| 505 | % This is important for independence | |
| 506 | % Example: CopyYY2XX(p) = PRE v>1 & p = yy THEN xx := p END --> Guard is #p.(p=yy) --> v>1 ; LTS Min Action is PRE p=yy THEN x := yy END; | |
| 507 | get_action(OpName,Action) :- get_operation_propositional_guards(OpName,_,Action). | |
| 508 | ||
| 509 | ||
| 510 | % we need just the variables that are read by the operation (constants will not be considered) | |
| 511 | b_get_read_write_vars(Operation,ReadGuardV,ReadActionV,ReadV,Write) :- | |
| 512 | b_get_read_write_vars_and_consts(false,Operation,ReadGuardV,ReadActionV,ReadV,Write). | |
| 513 | b_get_read_write_vars_and_consts(IncludeConstants,Operation,ReadGuardV,ReadActionV,ReadV,Write) :- | |
| 514 | b_get_read_write_guard_action(Operation,ReadGuard,ReadAction,Read,Write), | |
| 515 | b_get_machine_variables(TVars), | |
| 516 | (IncludeConstants==true | |
| 517 | -> b_get_machine_constants(TConsts), append(TConsts,TVars,TCV) % should we include get_global_identifiers ? | |
| 518 | ; TCV = TVars), | |
| 519 | get_texpr_ids(TCV,Vars), | |
| 520 | list_to_ord_set(Vars,Variables), | |
| 521 | ord_intersection(ReadGuard,Variables,ReadGuardV), | |
| 522 | ord_intersection(ReadAction,Variables,ReadActionV), | |
| 523 | ord_intersection(Read,Variables,ReadV). | |
| 524 | ||
| 525 | ||
| 526 | % ----------------------------------------------- | |
| 527 | % compute MAY/MUST write information (for LTSMin) | |
| 528 | % ----------------------------------------------- | |
| 529 | ||
| 530 | :- use_module(bsyntaxtree, [get_texpr_id/2, def_get_texpr_ids/2, is_truth/1, def_get_texpr_id/2]). | |
| 531 | ||
| 532 | % get read/write with may/must write info | |
| 533 | b_get_read_may_must_write(Operation,MustWriteV,MayWriteV) :- | |
| 534 | b_get_machine_operation(Operation,ReturnVars,_P,Body), | |
| 535 | b_get_read_write(Operation,_,WriteV), | |
| 536 | (is_eventb_event(Body) -> MayWriteV = [], | |
| 537 | WriteV = MustWriteV % in Event-B there are no conditions on the actions | |
| 538 | ; extract_must_write(Body,MustWriteV1) -> | |
| 539 | % remove return values: they are not global variables written to | |
| 540 | def_get_texpr_ids(ReturnVars,RV),list_to_ord_set(RV,SRV), %print(removing(SRV,Operation)),nl, | |
| 541 | ord_subtract(MustWriteV1,SRV,MustWriteV), | |
| 542 | ord_subtract(WriteV,MustWriteV,MayWriteV) | |
| 543 | ; add_internal_error('Extraction of Must-Write failed: ',extract_must_write(Body,_)), | |
| 544 | MustWriteV=[], MayWriteV=WriteV). | |
| 545 | /* | |
| 546 | b_get_read_may_must_write(Operation,ReadGuardV,ReadActionV,ReadV,MustWriteV,MayWriteV,WriteV) :- | |
| 547 | b_get_read_write_vars_and_consts(true,Operation,ReadGuardV,ReadActionV,ReadV,WriteV), | |
| 548 | b_get_machine_operation(Operation,ReturnVars,_P,Body), | |
| 549 | (is_eventb_event(Body) -> MayWriteV = [], MustWriteV=WriteV % in Event-B there are no conditions on the actions | |
| 550 | ; extract_must_write(Body,MustWriteV1) -> | |
| 551 | % remove return values: they are not global variables written to | |
| 552 | def_get_texpr_ids(ReturnVars,RV),list_to_ord_set(RV,SRV), %print(removing(SRV,Operation)),nl, | |
| 553 | ord_subtract(MustWriteV1,SRV,MustWriteV), | |
| 554 | ord_subtract(WriteV,MustWriteV,MayWriteV) | |
| 555 | ; add_internal_error('Extraction of Must-Write failed: ',extract_must_write(Body,_)), | |
| 556 | MustWriteV=[], MayWriteV=WriteV). | |
| 557 | */ | |
| 558 | is_eventb_event(b(E,_,_)) :- | |
| 559 | E = rlevent(_Name,_Section,_Status,_Params,_Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents). | |
| 560 | ||
| 561 | % compute the variables that must be written by an operation if it is enabled | |
| 562 | extract_must_write(b(Sub,_,_),MV) :- extract_must_write_aux(Sub,MV),!. | |
| 563 | extract_must_write(O,MV) :- add_internal_error('Call failed: ',extract_must_write(O,MV)),MV=[]. | |
| 564 | ||
| 565 | ||
| 566 | %extract_must_write_aux(P,V) :- functor(P,F,N), print(ex_aux(F,N)),nl,fail. | |
| 567 | extract_must_write_aux(assign(LHS,_),V) :- maplist(get_id,LHS,Vars), list_to_ord_set(Vars,V). | |
| 568 | extract_must_write_aux(assign_single_id(TID,_),[ID]) :- get_id(TID,ID). | |
| 569 | extract_must_write_aux(becomes_such(LHS,_),V) :- maplist(get_id,LHS,Vars), list_to_ord_set(Vars,V). | |
| 570 | extract_must_write_aux(becomes_element_of(LHS,_),V) :- maplist(get_id,LHS,Vars), list_to_ord_set(Vars,V). | |
| 571 | extract_must_write_aux(precondition(_,TBody),MV) :- extract_must_write(TBody,MV). | |
| 572 | extract_must_write_aux(assertion(_,TBody),MV) :- extract_must_write(TBody,MV). | |
| 573 | extract_must_write_aux(any(_,_,TBody),MV) :- extract_must_write(TBody,MV). | |
| 574 | extract_must_write_aux(let(_,_,TBody),MV) :- extract_must_write(TBody,MV). | |
| 575 | extract_must_write_aux(lazy_let_subst(_,_,TBody),MV) :- extract_must_write(TBody,MV). | |
| 576 | extract_must_write_aux(block(TBody),MV) :- extract_must_write(TBody,MV). | |
| 577 | extract_must_write_aux(choice([A]),MV) :- !, extract_must_write(A,MV). | |
| 578 | extract_must_write_aux(choice([A|T]),MV) :- | |
| 579 | extract_must_write(A,MV1), extract_must_write_aux(choice(T),MV2), ord_intersection(MV1,MV2,MV). | |
| 580 | extract_must_write_aux(if([I]),MV) :- !, get_texpr_expr(I,if_elsif(Cond,TBody)), | |
| 581 | (is_truth(Cond) -> extract_must_write(TBody,MV) ; MV=[]). % we have ELSE skip and then write nothing | |
| 582 | extract_must_write_aux(if([I|T]),MV) :- get_texpr_expr(I,if_elsif(_,TBody)), | |
| 583 | extract_must_write(TBody,MV1), extract_must_write_aux(if(T),MV2), ord_intersection(MV1,MV2,MV). | |
| 584 | extract_must_write_aux(select([SW]),MV) :- !, get_texpr_expr(SW,select_when(_,TBody)),extract_must_write(TBody,MV). | |
| 585 | extract_must_write_aux(select([SW|T]),MV) :- | |
| 586 | get_texpr_expr(SW,select_when(_,TBody)), extract_must_write(TBody,MV1), | |
| 587 | extract_must_write_aux(select(T),MV2),ord_intersection(MV1,MV2,MV). | |
| 588 | extract_must_write_aux(select(T,Else),MV) :- | |
| 589 | extract_must_write(Else,MV1), | |
| 590 | extract_must_write_aux(select(T),MV2),ord_intersection(MV1,MV2,MV). | |
| 591 | extract_must_write_aux(case(_,[],Else),MV) :- extract_must_write(Else,MV). | |
| 592 | extract_must_write_aux(case(E,[C|T],Else),MV) :- | |
| 593 | get_texpr_expr(C,case_or(_,TBody)), | |
| 594 | extract_must_write(TBody,MV1), | |
| 595 | extract_must_write_aux(case(E,T,Else),MV2),ord_intersection(MV1,MV2,MV). | |
| 596 | extract_must_write_aux(parallel([A]),MV) :- !, extract_must_write(A,MV). | |
| 597 | extract_must_write_aux(parallel([A|T]),MV) :- | |
| 598 | extract_must_write(A,MV1), extract_must_write_aux(parallel(T),MV2), ord_union(MV1,MV2,MV). | |
| 599 | extract_must_write_aux(sequence(S),MV) :- !, extract_must_write_aux(parallel(S),MV). | |
| 600 | extract_must_write_aux(skip,[]). | |
| 601 | extract_must_write_aux(external_subst_call(_,_),[]). % assume there is no guarantee that something is written | |
| 602 | extract_must_write_aux(while(_,_,_,_),[]). | |
| 603 | extract_must_write_aux(var(Parameters,TBody),MV) :- | |
| 604 | def_get_texpr_ids(Parameters,IDs), | |
| 605 | list_to_ord_set(IDs,MV2), | |
| 606 | extract_must_write(TBody,MV1), | |
| 607 | ord_subtract(MV1,MV2,MV). | |
| 608 | extract_must_write_aux(operation_call(TOperation,_,_),MustWriteV) :- | |
| 609 | def_get_texpr_id(TOperation,op(Operation)), | |
| 610 | b_get_read_may_must_write(Operation,MustWriteV,_). %and ideally cache values | |
| 611 | extract_must_write_aux(Other,[]) :- print(uncovered_subst_for_must_write(Other)),nl. | |
| 612 | ||
| 613 | get_id(b(function(A,_),_,_),ID) :- !, get_id(A,ID). | |
| 614 | get_id(TID,ID) :- get_texpr_id(TID,ID). | |
| 615 | ||
| 616 | % mainly used for LTS Min (uses LTSMin's definition of Action and (parameter-free) Guard): | |
| 617 | tcltk_read_write_matrix(list([list(['Operation','ReadsGuard','ReadsAction','MustWrite','MayWrite'])|Result])) :- | |
| 618 | findall(list([Operation,RG,RA,MustW,MayW]),b_get_read_may_must_write_for_ltsmin(Operation,RG,RA,MustW,MayW),Result). | |
| 619 | ||
| 620 | :- use_module(bsyntaxtree,[get_global_identifiers/1]). | |
| 621 | % obtains the read and written variables (constants, SETS and enumerated elements not included) | |
| 622 | % seperates the operations into parameter-independent guards and the rest, the Action | |
| 623 | :- use_module(predicate_debugger,[get_operation_propositional_guards/3]). | |
| 624 | :- use_module(probsrc(b_interpreter),[b_get_machine_operation_for_animation/6]). | |
| 625 | :- use_module(bmachine,[b_top_level_operation/1]). | |
| 626 | ||
| 627 | ||
| 628 | get_operation(Operation,Results,Paras) :- | |
| 629 | b_top_level_operation(Operation), | |
| 630 | b_get_machine_operation_for_animation(Operation,Results,Paras,_TB,_OT,true). | |
| 631 | ||
| 632 | b_get_read_may_must_write_for_ltsmin(Operation,ReadsGuard,ReadsAction,MustW,MayW) :- | |
| 633 | get_operation(Operation,Results,Paras), | |
| 634 | % LTSmin needs the constants in the read matrices; | |
| 635 | % if they are not included, it will transfer the uninitialised constants from the root state | |
| 636 | %b_get_machine_constants(TConsts), append(Paras,TConsts,TP), | |
| 637 | append(Results, Paras, ResultsAndParas), | |
| 638 | get_texpr_ids(ResultsAndParas,TPIds), | |
| 639 | get_global_identifiers(Global), | |
| 640 | append(TPIds,Global,PIDs),list_to_ord_set(PIDs,VarsToIgnore), % the VarsToIgnore should not be included in the matrix | |
| 641 | b_get_read_may_must_write(Operation,MustW,MayW), % we ignore the info about guards and actions: LTS Min has another definition of what a guard is than b_get_read_may_must_write | |
| 642 | get_operation_propositional_guards(Operation,Guards,RestBody), % obtain LTSMin guards, which are independent of the parameters | |
| 643 | get_accessed_vars(RestBody,VarsToIgnore,_Modified,ReadsAction), % this computes the ReadsAction the LTSMin way | |
| 644 | %format('READS ACTION for ~w ~n ~w~n',[Operation,ReadsAction]), | |
| 645 | conjunct_predicates(Guards,G), | |
| 646 | find_identifier_uses(G,VarsToIgnore,ReadsGuard). | |
| 647 | % (op_has_parameters(Operation) | |
| 648 | % -> ReadsAction = FullReads % guards on parameters may be projected away; leading to implicit reads in actions | |
| 649 | % % TO DO: convert operations into normal form; until this is done: simply return full reads | |
| 650 | % ; ReadsAction = RA). | |
| 651 | ||
| 652 | %op_has_parameters(OpName) :- | |
| 653 | % b_get_machine_operation_for_animation(OpName,_Results,Paras,_TB,_OT,true), | |
| 654 | % Paras = [_|_]. | |
| 655 | ||
| 656 | ||
| 657 | rw_ord_intersection('$all',B,R) :- !,R=B. | |
| 658 | rw_ord_intersection(A,'$all',R) :- !,R=A. | |
| 659 | rw_ord_intersection(A,B,R) :- ord_intersection(A,B,R). | |
| 660 | ||
| 661 | ||
| 662 | % compute the variables that are written by at least one operation: | |
| 663 | b_get_written_variables(WrittenVariables) :- | |
| 664 | findall(Var, | |
| 665 | (b_top_level_operation(Operation), | |
| 666 | %get_operation(Operation,_Results,_Paras), | |
| 667 | b_get_read_write(Operation,_,WriteV), | |
| 668 | member(Var,WriteV) | |
| 669 | ),Vars), | |
| 670 | sort(Vars,WrittenVariables). | |
| 671 | ||
| 672 | % compute the variables that are read by at least one operation: | |
| 673 | b_get_read_variables(ReadVariables) :- | |
| 674 | findall(Var, | |
| 675 | (b_top_level_operation(Operation), | |
| 676 | b_get_read_write(Operation,ReadV,_), | |
| 677 | member(Var,ReadV) | |
| 678 | ),Vars), | |
| 679 | sort(Vars,ReadVariables). | |
| 680 | % compute the variables that are read by at least one operation: | |
| 681 | b_get_read_guard_variables(ReadVariables) :- | |
| 682 | findall(Var, | |
| 683 | (b_top_level_operation(Operation), | |
| 684 | b_get_operation_read_guard_vars(Operation,true,ReadV), | |
| 685 | member(Var,ReadV) | |
| 686 | ),Vars), | |
| 687 | sort(Vars,ReadVariables). | |
| 688 | ||
| 689 | % cannot be run in bmachine_static_checks as operations are not yet precompiled | |
| 690 | check_all_variables_written :- | |
| 691 | b_get_written_variables(WrittenVariables), | |
| 692 | b_get_machine_variables(TVars), | |
| 693 | member(TVar,TVars), | |
| 694 | get_texpr_id(TVar,Var), | |
| 695 | \+ ord_member(Var,WrittenVariables), | |
| 696 | add_warning(check_all_variables_written,'Variable is written by no operation (consider defining is as a constant): ',Var,TVar), | |
| 697 | fail. | |
| 698 | check_all_variables_written. | |
| 699 | ||
| 700 | % compute a matrix which shows for variables who reads and modifies them: | |
| 701 | tcltk_variable_read_write_matrix(Warn,list([list(['Variable','Read by','Written by'])|Result])) :- | |
| 702 | findall(list([Variable,Reads,Writes]), | |
| 703 | get_read_write_ops_for_variable(Variable,Reads,Writes),Result), | |
| 704 | (Warn=no_check -> true ; check_all_variables_written). | |
| 705 | ||
| 706 | get_read_write_ops_for_variable(Var,ReadOps,WriteOps) :- | |
| 707 | b_get_machine_variables(TVars), member(TVar,TVars), get_texpr_id(TVar,Var), | |
| 708 | findall(Op,(b_top_level_operation(Op),b_get_read_write(Op,Reads,_),ord_member(Var,Reads)),ReadOps), | |
| 709 | findall(Op,(b_top_level_operation(Op),b_get_read_write(Op,_,Writes),ord_member(Var,Writes)),WriteOps). | |
| 710 | ||
| 711 | ||
| 712 | % -------------------- READ/WRITE VARIABLE ANALYSIS GRAPH ------------------------- | |
| 713 | ||
| 714 | :-use_module(dot_graph_generator,[gen_dot_graph/6]). | |
| 715 | tcltk_dot_variable_modification_analysis(File) :- | |
| 716 | gen_dot_graph(File,b_read_write_info,var_op_node_predicate,var_mod_pred,none,none). | |
| 717 | ||
| 718 | ||
| 719 | :- use_module(tools_strings,[ajoin/2]). | |
| 720 | :- use_module(preferences,[get_preference/2]). | |
| 721 | var_op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- | |
| 722 | b_get_written_variables(WrittenVariables), | |
| 723 | b_get_read_variables(ReadVariables), | |
| 724 | b_get_read_guard_variables(ReadGrdVariables), | |
| 725 | SubGraph=none, | |
| 726 | Color='RoyalBlue4', | |
| 727 | b_is_variable(NodeID), | |
| 728 | (ord_member(NodeID,ReadGrdVariables) | |
| 729 | -> Style=none | |
| 730 | ; get_preference(dot_var_mod_hide_only_written,false), | |
| 731 | Style=dotted | |
| 732 | ), | |
| 733 | (\+ ord_member(NodeID,WrittenVariables) | |
| 734 | -> Shape=invtrapezium, ajoin([NodeID,'\\n (NOT WRITTEN)'],NodeDesc) | |
| 735 | ; \+ ord_member(NodeID,ReadVariables) | |
| 736 | -> Shape=trapezium, ajoin([NodeID,'\\n (NOT READ)'],NodeDesc) | |
| 737 | ; Shape=box, NodeDesc=NodeID | |
| 738 | ). | |
| 739 | var_op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- | |
| 740 | b_top_level_operation(NodeID), | |
| 741 | %b_get_read_write(NodeID,_,Writes), dif(Writes,[]), % do not show query operations | |
| 742 | SubGraph=none, Shape=rect, Style='filled,rounded', | |
| 743 | NodeDesc=NodeID, Color=gray90. | |
| 744 | ||
| 745 | ||
| 746 | :- use_module(translate,[translate_bexpression_with_limit/3]). | |
| 747 | :- public var_mod_pred/5. | |
| 748 | var_mod_pred(OpNodeID,Label,SuccID,Color,Style) :- Color=red4, Style=solid, | |
| 749 | b_get_read_guard_variables(ReadVariables), | |
| 750 | b_get_read_may_must_write(OpNodeID,MustWrite,_), | |
| 751 | member(SuccID,MustWrite), | |
| 752 | (get_preference(dot_var_mod_hide_only_written,true) | |
| 753 | -> ord_member(SuccID,ReadVariables) ; true), | |
| 754 | (get_assignment_value(OpNodeID,SuccID,Val) | |
| 755 | -> translate_bexpression_with_limit(Val,30,VS), | |
| 756 | ajoin([':= \\n',VS],Label) | |
| 757 | ; Label = writes). | |
| 758 | var_mod_pred(OpNodeID,Label,SuccID,Color,Style) :- Color=goldenrod, Label='may write',Style=dotted, | |
| 759 | b_get_read_guard_variables(ReadVariables), | |
| 760 | b_get_read_may_must_write(OpNodeID,_,MayWrite), | |
| 761 | member(SuccID,MayWrite), | |
| 762 | (get_preference(dot_var_mod_hide_only_written,true) | |
| 763 | -> ord_member(SuccID,ReadVariables) ; true). | |
| 764 | var_mod_pred(NodeID,Label,SuccOpID,Color,Style) :- Color=azure4, Style=solid, | |
| 765 | %b_get_read_write(SuccOpID,Reads,_), | |
| 766 | %b_get_read_may_must_write_for_ltsmin(SuccOpID,ReadsGuard,_,_,_), | |
| 767 | b_get_operation_read_guard_vars(SuccOpID,true,ReadsGuard), | |
| 768 | member(NodeID,ReadsGuard), | |
| 769 | (get_decisive_predicate_from_guard(SuccOpID,NodeID,_Pred,Op,Val) | |
| 770 | -> translate_bexpression_with_limit(Val,30,VS), | |
| 771 | ajoin([Op,'\\n',VS],Label) | |
| 772 | ; Label = reads). | |
| 773 | ||
| 774 | % try to find relevant, decisive checks from guard | |
| 775 | get_decisive_predicate_from_guard(Operation,Variable,TPred,Op,TVal) :- | |
| 776 | get_operation_guard(Operation,G), | |
| 777 | member_in_conjunction(TPred,G), | |
| 778 | get_texpr_expr(TPred,Pred), | |
| 779 | is_decisive(Pred,Variable,Op,TVal). | |
| 780 | ||
| 781 | is_decisive(equal(TID,VAL),Variable,'=',VAL) :- get_texpr_id(TID,Variable), simple_val(VAL). | |
| 782 | is_decisive(equal(VAL,TID),Variable,'=',VAL) :- get_texpr_id(TID,Variable), simple_val(VAL). | |
| 783 | % TO DO: other checks ? not_equal, greater, ... | |
| 784 | simple_val(b(V,_,_)) :- simple_val2(V). | |
| 785 | simple_val2(empty_set). | |
| 786 | simple_val2(empty_sequence). | |
| 787 | simple_val2(boolean_true). | |
| 788 | simple_val2(boolean_false). | |
| 789 | simple_val2(integer(_)). | |
| 790 | simple_val2(string(_)). | |
| 791 | simple_val2(max_int). | |
| 792 | simple_val2(min_int). | |
| 793 | simple_val2(value(_)). | |
| 794 | ||
| 795 | get_assignment_value(Operation,Variable,Val) :- | |
| 796 | get_action(Operation,TAction), | |
| 797 | get_texpr_expr(TAction,Action), | |
| 798 | get_assign_val(Action,Variable,Val). | |
| 799 | ||
| 800 | get_assign_val(assign_single_id(TID,Val),ID,Val) :- | |
| 801 | get_texpr_id(TID,ID),!, | |
| 802 | (simple_val(Val) -> true ; simple_modification(Val,ID)). | |
| 803 | get_assign_val(any(_,_,TBody),Var,Val) :- get_texpr_expr(TBody,Body), get_assign_val(Body,Var,Val). | |
| 804 | get_assign_val(select([b(select_when(_,TBody),_,_)]),Var,Val) :- | |
| 805 | get_texpr_expr(TBody,Body), get_assign_val(Body,Var,Val). | |
| 806 | get_assign_val(parallel(Bodies),Var,Val) :- member(TBody,Bodies), | |
| 807 | get_texpr_expr(TBody,Body), get_assign_val(Body,Var,Val). | |
| 808 | % TO DO: sequence, ... | |
| 809 | ||
| 810 | simple_modification(TExpr,Var) :- get_texpr_expr(TExpr,Expr), | |
| 811 | simple_modification_aux(Expr,Var). | |
| 812 | simple_modification_aux(add(A,B),Var) :- simple_binop(A,B,Var). | |
| 813 | simple_modification_aux(minus(A,B),Var) :- simple_binop(A,B,Var). | |
| 814 | simple_modification_aux(multiplication(A,B),Var) :- simple_binop(A,B,Var). | |
| 815 | ||
| 816 | simple_binop(TID,Val,Var) :- get_texpr_id(TID,Var), simple_val(Val). | |
| 817 | simple_binop(Val,TID,Var) :- get_texpr_id(TID,Var), simple_val(Val). | |
| 818 |