bmachine_static_checks

atomic_subst(b(S,_,_)) :- atomic_subst2(S).

atomic_subst2(skip).

atomic_subst2(assign(_,_)).

atomic_subst2(assign_single_id(_,_)).

atomic_subst2(becomes_element_of(_,_)).

boolean_operator(conjunct).

boolean_operator(disjunct).

boolean_operator(implication).

boolean_operator(equivalence).

check_aux(function(b(Func,_,_I1),_Arg),_,I2,Ctxt) :- % _I1 sometimes unknown
    % TO DO: check if Info contains WD flag
    check_is_partial_function(Func,I2,Ctxt).

check_concrete_constants :- is_concrete_constants_state_id(ID),!,
    check_values_in_state(ID).

check_concrete_constants.

check_definition_clashes(SortedAllIds) :-
    Scope=[variables],
    b_get_typed_definition(Name,Scope,TExpr),
    % TODO: adapt type_check_definitions to return definitions with paras and add paras to list of Ids
    %print(check(Name,SortedAllIds)),nl,
    map_over_typed_bexpr_with_names(bmachine_static_checks:check_introduced_ids('DEFINITION',Name,SortedAllIds),TExpr).

check_initialisation_order(b(Subst,subst,Info),AllVars,AlreadyInit,OutInit) :-
    check_initialisation_order2(Subst,Info,AllVars,AlreadyInit,OutInit),!.

check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit) :-
    % print('CHCK '), translate:print_subst(Subst),nl,
    get_accessed_vars(Subst,[],Modifies,Reads),
    check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit).

check_initialisation_order2(choice([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !,
    check_initialisation_order(First,AllVars,AlreadyInit,OutInit), % we pick the output of the first choice
    (T=[] -> true ; check_initialisation_order(b(choice(T),subst,Info),AllVars,AlreadyInit,_)).

check_initialisation_order2(parallel([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !,
    check_initialisation_order(First,AllVars,AlreadyInit,OutInit1), % we pick the output of the first choice
    (T=[] -> OutInit=OutInit1
    ; check_initialisation_order2(parallel(T),Info,AllVars,AlreadyInit,OutInitRest),
    ord_union(OutInit1,OutInitRest,OutInit)
).

check_initialisation_order2(init_parallel(S),Info,AllVars,AlreadyInit,OutInit) :- !,
    check_initialisation_order(b(parallel(S),subst,Info),AllVars,AlreadyInit,OutInit).

check_initialisation_order2(sequence([First|T]),Info,AllVars) --> !,
    check_initialisation_order(First,AllVars),
    ({T=[]} -> [] ; check_initialisation_order(b(sequence(T),subst,Info),AllVars)).

check_initialisation_order2(any(_Ids,Pred,Subst),_Info,AllVars,AlreadyInit,OutInit) :- !,
    find_identifier_uses(Pred,[],Reads),
    check_subst_or_pred(Pred,[],Reads,AllVars,AlreadyInit,_), % check predicate reads are ok
    check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit).

check_introduced_ids(Section,SectionID,SortedAllIds,TExpr,TNames) :-
    \+ ignore_constructor(TExpr),
    (member(TName,TNames),
    clash_warnings('local variable',SortedAllIds,Section,SectionID,TName)
    ; removed_identifier(TExpr,TName),
    clash_warnings('(removed) local variable',SortedAllIds,Section,SectionID,TName)
% TODO: also check duplicate_id_hides info fields ?
).

check_is_partial_function(value(Val),Info,Ctxt) :- nonvar(Val), Val=avl_set(AVL),
    is_not_avl_partial_function(AVL,DuplicateKey),!,
    avl_size(AVL,Size),
    translate_bvalue_with_limit(DuplicateKey,80,DKS),
    ajoin(['Relation of size ', Size, ' is not a function (value for ',Ctxt, '); duplicate key: '],Msg),
    add_warning(bmachine_static_checks,Msg,DKS,Info).

check_is_partial_function(_,_,_).

check_name_clashes(Machine) :-
    debug_println(10,'Checking for name clashes'),
    get_all_machine_ids(Machine,SortedAllIds),
    % for each operation, compare the parameter names with existing vars/constants
    get_section(operation_bodies,Machine,Operations),
    maplist(op_name_clashes(SortedAllIds),Operations),
    get_section(definitions,Machine,Defs),
    maplist(def_name_clashes(SortedAllIds),Defs).

check_operation_body(Body,OpID) :- b_top_level_operation(OpID),
    \+ b_top_level_feasible_operation(OpID),
    add_warning(bmachine_static_checks,'Infeasible body for operation:',OpID,Body),
    fail.

check_operation_body(Body,OpID) :-
    (map_over_typed_bexpr(bmachine_static_checks:check_operation_body_var(OpID),Body),fail ; true).

check_operation_body_clashes(AllIds,Operation,TSubst) :-
    get_texpr_expr(TSubst,Subst),
    (local_variable_clash(Subst,TSubst,AllIds,Operation);
    illegal_op_call(Subst,Operation)).

check_operation_body_var(OpID,b(var(Parameters,Body),subst,_Pos)) :-
    get_texpr_ids(Parameters,Ps), sort(Ps,Uninitialised),
    get_accessed_vars(Body,[],_Modifies,Reads),
    ord_intersection(Uninitialised,Reads,URead),
    URead \= [],
    member(TID,Parameters), get_texpr_id(TID,ID),
    member(ID,URead),
    ajoin(['Possibly reading uninitialised variable in operation ',OpID,' : '],Msg),
    add_warning(bmachine_static_checks,Msg,ID,TID).

check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit) :-
    ord_union(Modifies,AlreadyInit,OutInit), % after Subst we have initialised OutInit
    % below is already checked by type checker:
    %ord_subtract(Modifies,AllVars,IllegalAssignments),
    %(IllegalAssignments=[] -> true
    % ; add_warning(bmachine_static_checks,'INITIALISATION writes illegal variables: ',IllegalAssignments,Subst)),
    ord_intersection(Reads,AllVars,ReadFromSameMachine),
    (atomic_subst(Subst)
    -> ord_subtract(ReadFromSameMachine,AlreadyInit,IllegalReads)
    ; ord_subtract(ReadFromSameMachine,OutInit,IllegalReads) % we use OutInit: there could be an if with sequence inside
    ),
    (IllegalReads=[] -> true
    ; add_warning(bmachine_static_checks,'INITIALISATION reads variables which are not yet initialised: ',IllegalReads,Subst)).

check_symbolic_value(Ctxt,b(E,T,I)) :- check_aux(E,T,I,Ctxt).

check_symbolic_values(Var,Ctxt) :- var(Var),!,
    add_error(bmachine_static_checks,'Value is a variable',Ctxt).

check_symbolic_values(closure(_,_,Body),Ctxt) :- !,
    debug_format(19,'Checking symbolic value for ~w~n',[Ctxt]),
    map_over_typed_bexpr(check_symbolic_value(Ctxt),Body).

check_symbolic_values(_,_).

check_top_level(implication(_,B,C),MachName,SECT) :-
    (composed_predicate(B) ; composed_predicate(C)),!,
    add_warning(bmachine_static_checks,'Top-level implication (=>) in clause: ',MachName:SECT).

check_top_level(disjunct(_,B,C),MachName,SECT) :-
    (composed_predicate(B) ; composed_predicate(C)),!,
    add_warning(bmachine_static_checks,'Top-level disjunction (or) in clause: ',MachName:SECT).

check_top_level(equivalence(_,B,C),MachName,SECT) :-
    (composed_predicate(B) ; composed_predicate(C)),!,
    add_warning(bmachine_static_checks,'Top-level equivalence (<=>) in clause: ',MachName:SECT).

check_unused_ids :-
    b_is_unused_constant(ID),
    get_constant_span(ID,Span),
    % TO DO: check if the constant is used to define other used constants
    (get_preference(filter_unused_constants,true)
    -> add_message(bmachine_static_checks,'This constant is not used outside of the PROPERTIES/axioms (and is filtered away because FILTER_UNUSED preference is TRUE): ',ID,Span)
    ; add_message(bmachine_static_checks,'This constant is not used outside of the PROPERTIES/axioms: ',ID,Span)
    ),
    fail.

check_unused_ids.

check_values_in_state(ID) :- debug_format(19,'Checking values in state with id = ~w~n',[ID]),
    visited_expression(ID,State),
    state_corresponds_to_set_up_constants(State,EState),
    member(bind(VarID,Value),EState),
    check_symbolic_values(Value,VarID),
    fail.

check_values_in_state(_).

clash_local_warnings(AllIds,OperationId,Name,Pos) :-
    my_ord_member(Name,Class,Descr,AllIds), !,
    % we could check and see if Name is really visible from this location!
    % (see public_examples/B/Other/LustreTranslations/UMS_verif/M_UMS_verif.mch)
    ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a local variable in operation "', OperationId,'".'], Msg),
    add_warning(bmachine_static_checks,Msg,'',Pos).

clash_warnings(Context,AllIds,OpOrDef,OperationId,TName) :-
    get_texpr_id(TName,Name),
    my_ord_member(Name,Class,Descr,AllIds), !,
    ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a ',
    Context, ' in ',OpOrDef,' "', OperationId,'".'], Msg),
    add_warning(bmachine_static_checks,Msg,'',TName).

composed_predicate(A) :- functor(A,Operator,N),
    boolean_operator(Operator),
    % Some binary operators (conjunct, disjunct) can have a varying number of arguments.
    % See predicates associative_functor/1 and unflatten_assoc/4 in btypechecker.
    N >= 2.

def_name_clashes(AllIds,definition_decl(Name,DefType,_DefPos,Args,_RawExpr,_Deps)) :- !,
    (is_external_function_name(Name)
    -> true % do not check external predicates, functions, subst
    % they are not written by user and possibly not used and definitions are virtual and not used anyway
    ; findall(b(identifier(ID),any,[nodeid(IdPos)]),
    member(identifier(IdPos,ID),Args),ArgIds), % args can sometimes not be identifiers; see test 1711
    debug_println(4,checking_def(Name,DefType,Args,ArgIds)),
    include(clash_warnings('DEFINITION parameter',AllIds,'DEFINITION',Name),ArgIds,_ArgsCausingWarning)
% TO DO: check Body; for this we need a map_over_raw_expression to detect local variables introduced !
).

def_name_clashes(_,D) :- print(unknown_def(D)),nl.

esc_aux :-
    b_machine_name(Name),
    b_get_main_filename(Filename),
    get_modulename_filename(Filename,ModuleName),
    Name \= ModuleName,
    (atom_concat('MAIN_MACHINE_FOR_',RealName,Name) % see dummy_machine_name in bmachine_construction
    -> RealName \= ModuleName
    ; is_dummy_machine_name(Name,Filename)
    -> fail % dummy Rules DSL or Alloy machine name, do not create warning
    ; true
    ),
    (b_get_machine_header_position(Name,Span) -> true
    ; Span = src_position_with_filename(1,1,1,Filename)),
    get_specification_description(machine,MCH),
    ajoin(['Filename ',ModuleName,' does not match name of ', MCH, ': '],Msg),
    add_warning(bmachine_static_checks,Msg,Name,Span),
    fail.

esc_aux :- debug_println(19,checking_identifiers_for_clashes),
    full_b_machine(Machine),
    local_quantified_variable_clashes(Machine),
    fail.

esc_aux :- machine_type(MachName,abstract_machine),
    machine_operations(MachName,Ops),
    member(identifier(Span,OpName),Ops),
    atom_codes(OpName,Codes), member(46,Codes), % "." element of name
    % Section 7.23, paragraph 2 of Atelier-B handbook: in abstract machine we cannot use renamed operation names
    ajoin(['Operation name in abstract machine ',MachName,' is composed: '],Msg),
    add_warning(bmachine_static_checks,Msg,OpName,Span),
    fail.

esc_aux :- debug_println(19,checking_operation_bodies),
    b_get_machine_operation(ID,_Res,_TParas,Body,_OType,_Pos),
    check_operation_body(Body,ID),
    fail.

esc_aux :-
    check_concrete_constants,
    check_unused_ids.

extended_static_check_machine :-
    check_all_variables_written,
    esc_aux.

generate_uninitialised_warning([],_) :- !.

generate_uninitialised_warning(Vars,Initialisation) :-
    Msg='Machine may not initialise some of its variables: ',
    add_warning(bmachine_static_checks,Msg,Vars,Initialisation).

get_all_machine_ids(Machine,SortedAllIds) :-
    % get all variables and constants that might clash
    get_section_ids(abstract_variables,Machine,'variable',AbsVars),
    get_section_ids(concrete_variables,Machine,'variable',ConcVars),
    get_section_ids(abstract_constants,Machine,'constant',AbsCons),
    get_section_ids(concrete_constants,Machine,'constant',ConcCons),
    get_section_ids(deferred_sets,Machine,'set',DefSets),
    get_section_ids(enumerated_sets,Machine,'set',EnumSets),
    get_section_ids(enumerated_elements,Machine,'set element',EnumElems),
    % enumerated b_get_named_machine_set(GlobalSetName,ListOfConstants) + b_get_machine_set(S)
    append([AbsVars,ConcVars,AbsCons,ConcCons,DefSets,EnumSets,EnumElems],AllIds),
    keyword_clash(AllIds),
    sort(AllIds,SortedAllIds).

get_descr(Pos,Section,Descr) :-
    (extract_span_description(Pos,Descr) -> true
    ; ajoin(['from section ',Section],Descr) ).

get_machine_variables(Machine,SortedAllVars) :-
    % get all variables that should be initialised
    get_section(abstract_variables,Machine,AbsVars),
    get_section(concrete_variables,Machine,ConcVars),
    append(AbsVars,ConcVars,TAllVars),
    get_texpr_ids(TAllVars,AllVars),
    sort(AllVars,SortedAllVars).

get_section_ids(Section,Machine,Class,ResultList) :-
    get_section(Section,Machine,Vars),
    findall(machine_id(ID,Class,Pos,Section),
    (member(TID,Vars),get_texpr_id(TID,ID),get_texpr_info(TID,Pos)),ResultList).

get_sub_predicate(Clause,Pred,Kind,Name,SubPred) :-
    conjunction_to_list(Pred,Preds),
    l_get_sub_predicate(Clause,Preds,Kind,Name,SubPred).

get_typed_section(Kind,Name,SubPred) :-
    b_get_properties_from_machine(P), get_specification_description(properties,PS),
    get_sub_predicate(PS,P,Kind,Name,SubPred).

get_typed_section(Kind,Name,SubPred) :-
    b_get_invariant_from_machine(P), get_specification_description(invariants,PS),
    get_sub_predicate(PS,P,Kind,Name,SubPred).

get_typed_section(Kind,Name,SubPred) :-
    get_specification_description(assertions,APS), ajoin(['(dynamic) ',APS],AS),
    b_get_dynamic_assertions_from_machine(Ps),
    l_get_sub_predicate(AS,Ps,Kind,Name,SubPred).

get_typed_section(Kind,Name,SubPred) :-
    get_specification_description(assertions,APS), ajoin(['(static) ',APS],AS),
    b_get_static_assertions_from_machine(Ps),
    l_get_sub_predicate(AS,Ps,Kind,Name,SubPred).

get_typed_section(operation,OpName,P) :- b_get_machine_operation(OpName,_Results,_Parameters,P).

ignore_constructor(b(recursive_let(_,_),_,_)).

illegal_op_call(operation_call(CalledOperation,Results,_Parameters),Operation) :-
    member(TID,Results), \+ get_texpr_id(TID,_),
    (get_texpr_id(CalledOperation,op(CalledId)) -> true ; CalledId=CalledOperation),
    ajoin(['Return value of operation call to ',CalledId,' must be stored in identifier within:'],Msg),
    add_error(bmachine_static_checks,Msg,Operation,TID).

initialises_all_variables(Machine) :-
    get_section(initialisation,Machine,Initialisation),
    % check wich variables are read / modified by the initialisation
    get_accessed_vars(Initialisation,[],Modifies,_Reads),
    get_machine_variables(Machine,SortedAllVars),
    % check for each variable, if the initialisation modifies it
    exclude(is_initialised(Modifies),SortedAllVars,Uninitialised),
    % generate a warning if unitialised is not empty
    generate_uninitialised_warning(Uninitialised,Initialisation),
    % now check order of initialisation sequences
    check_initialisation_order(Initialisation,SortedAllVars,[],_).

introduced_ids(forall(IDs,_,_),IDs).

introduced_ids(exists(IDs,_),IDs). % % are there more relevant cases? TODO: use syntaxtraversion

introduces_local_variable(var(Parameters,_),ID) :-
    % currently B-interpreter cannot correctly deal with this in the context of operation_call
    member(TID,Parameters), get_texpr_id(TID,ID).

is_dummy_machine_name(Name,_) :- atom_prefix('__RULES_MACHINE_Main',Name).

is_dummy_machine_name(alloytranslation,_) :- animation_minor_mode(alloy).

is_dummy_machine_name('DEFINITION_FILE',Filename) :- classical_b_mode,
    get_filename_extension(Filename,'def').

is_initialised(Modifies,Id) :-
    memberchk(Id,Modifies).

keyword_clash(AllIds) :-
    member(machine_id(Name,Class,Pos,Section),AllIds),
    is_b_keyword(Name,_),
    get_descr(Pos,Section,Descr),
    ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a classical B keyword (may lead to unexpected parse or type errors when entering formulas unless you surround it by backquotes: `',Name,'`).'], Msg),
    (classical_b_mode
    -> add_message(bmachine_static_checks,Msg,'',Pos) % user probably uses new backquote syntax already
    ; add_warning(bmachine_static_checks,Msg,'',Pos)
    ),
    fail.

keyword_clash(_).

l_get_sub_predicate(Clause,Preds,Kind,Name,SubPred) :-
    member(SubPred,Preds),
    (get_texpr_label(SubPred,Label)
    -> Kind = predicate, ajoin([Label,'" in clause "',Clause],Name)
    ; Kind = clause, Name=Clause).

local_quantified_variable_clashes(Machine) :-
    get_all_machine_ids(Machine,SortedAllIds),
    (get_typed_section(Sec,SecID,Pred),
    debug_println(19,checking_local_quantified_variable_clashes(Sec,SecID)),
    map_over_typed_bexpr_with_names(bmachine_static_checks:check_introduced_ids(Sec,SecID,SortedAllIds),Pred)
    ;
    check_definition_clashes(SortedAllIds)
    ),
    fail.

local_quantified_variable_clashes(_).

local_variable_clash(Subst,TSubst,AllIds,Operation) :-
    introduces_local_variable(Subst,ID),
    clash_local_warnings(AllIds,Operation,ID,TSubst).

my_ord_member(Name,Class,Descr,[machine_id(Name1,_,_,_)|T]) :-
    Name @> Name1, !,
    my_ord_member(Name,Class,Descr,T).

my_ord_member(Name,Class,Descr,[machine_id(Name,Class,Pos,Section)|_]) :-
    get_descr(Pos,Section,Descr).

op_name_clashes(AllIds,Operation) :-
    get_texpr_expr(Operation,operation(IdFull,Results,Params,Subst)),
    %get_texpr_id(IdFull,op(Id)),
    IdFull = b(identifier(op(Id)),Type,Info),
    (get_preference(clash_strict_checks,true)
    -> include(clash_warnings('Operation name',AllIds,operation,Id),[b(identifier(Id),Type,Info)],_NameCausingWarning) % fix PROB-60
    ; true),
    include(clash_warnings('Operation parameter',AllIds,operation,Id),Params,_ParamsCausingWarning),
    include(clash_warnings('Operation result variable',AllIds,operation,Id),Results,_ResultsCausingWarning),
    (map_over_typed_bexpr(bmachine_static_checks:check_operation_body_clashes(AllIds,Id),Subst),fail ; true).

removed_identifier(b(_,_,Infos),TId) :-
    member(was(WAS),Infos),
    introduced_ids(WAS,IDs),
    % this happens in EnumSetClash2.mch
    member(TId,IDs).

static_check_main_machine(Machine) :-
    debug_println(19,'Running static machine checks'),
    initialises_all_variables(Machine),
    check_name_clashes(Machine).

toplevel_raw_predicate_sanity_check(invariant,MachName,RawPredicate,Infos) :-
    member(has_variables,Infos), % otherwise it is ok to have just a single disjunt, implication,...
    check_top_level(RawPredicate,MachName,'INVARIANT'),
    fail.

toplevel_raw_predicate_sanity_check(properties,MachName,RawPredicate,Infos) :-
    member(has_constants,Infos), % otherwise it is ok to have just a single disjunt, implication,...
    check_top_level(RawPredicate,MachName,'PROPERTIES'),
    fail.

toplevel_raw_predicate_sanity_check(_,_,_,_).