% SYMBOLIC EXECUTION
%   copyright Peter H. Roosen-Runge, 1991-2007

% Ver. 2.0, March 5, 1991: handles assignment statements, goals, and IFs. 
%      2.3, Feb. 24, 1992:  Statements can *begin* with an assertion.
%      2.3.1, March 6:  Initial values supplied automatically (again!)
%      3.1 Feb. 27, 1998: uses getTheories to load simplification rules.
%      3.1.2 March 20: clean expressions before converting to term.
%                     allow white space between // and {
%      4.0  Dec. 22, 1998: reads "contracts" and procedure calls
%      4.2.4 March 8: test if assertion is impossible
%      4.2.4.3 March 19: recompiled with clean.prolog v 1.4
%                    allows A[E] in expressions.
%                  still doesn't do parallel assignment
%      4.2.4.6 April 6: print "{", "}" around a statement block
%      4.2.4.8 April 9: repaired procedure post-condition processing
%      4.2.4.9 April 11: simplify if and else conditions before checking
%      4.2.5 March 19, 2000: added multifile and dynamic directives,
%                    processes 'simplification.rules' as a theory file
%                    rather than consulting it. makefun repaired to
%                    allow general pre-conditions as well as identities.
%      4.2.5.1 March 25: checks if simplification.rules exists before
%           trying to open it.

%      4.2.6   March 29: symex repaired to handle X or Y conditions
%      5.0     August 25: allow while loops with invariants
%      5.0A    March 31, 2002: attempt to repair from 5.3
%      5.3ASWI February 24, 2007: SWI version
% =====================================================================
% Reads an initial condition in the form
% //{ C and x = e1  and y = e2 . . . etc. } 
% or //{x = e1  and y = e2 . . . and C}
% where the ei are expressions specifying the initial values of variables
% in the code which follows and C is a pre-condition on the initial values.
% The initial condition is followed by a sequence of assignment or 
% IF-statements which are 'symbolically executed'.

% a program fragment can be preceded by one more procedure specification 
% in the form
%   //{ precondition }
%   void IDENTIFIER(ARGS);
%   //{ postcondition}

% The parameters in the pre- and post-conditions must be in upper case.


% symbex reports the precondition which holds before THEN or ELSE branches
% and notes branches which are never or always taken.
% Allowable statement forms --
%		V = Expression ;
%		if (B) statement
%		if (B) statement1 else statement2
%               while(B) //{ invariant } statement			
%
%		{ statements }

% N. B. The right-hand sides of the initial conditions *must not*
% contain occurrences (as atoms) of any variables which occur on the left
% of any equality. You can however use conditions such as x = x(0).

% An assertion in the form { proposition } can precede a statement
% or follow the entire code fragment.
% If one occurs, a test is made to see if the previous post-condition
% implies this assertion and the result of the test is reported.
%
% symbex searches the home, working, and working directories for
% arithmetic.simp, equality.simp, and logic.simp, and loads a file 
% "simplification.rules" from the working directory, if there is one.
% 
% ==============================================================

% error(Message) :- nl, write('!! '), write(Message), nl, halt.
% user_error_handler(_,_,_,_) :- error('Something wrong.').
%:-unknown(_,fail).
%:- nofileerrors.  (handled in getTheories)

:- multifile '->>'/2.  :- dynamic '->>'/2.

:- ensure_loaded([qlib(files), qlib(lineio), qlib(ctypes), qlib(occurs) ]).
% qlib(charsio), qlib(lists), qlib(basics) not needed in SWI

% For consistency, operator declarations used by wang, taut, simp, symbex, and
% quants.

:-op(999,xfx, '!'). % used to separate condition from current function.
:-op(995,xfx, '->>').  % simplification
:-op(995,xfy,'>>').    % sequent
:-op(995,xfy, '::').  % separate parts of a quantified expression
:-op(990, yfx, iff).  % Left-associative (yfx) for consistency with
                      % commutative arithmetic operators.
:-op(1199, xfx, if).  % separate condition from rule.

:-op(990,yfx,implies). % for consistency with iff
:-op(980,yfx, [or, cor]).
:-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
:-op(960,yfx,[and, cand, div, mod]).
:-op(950,fy,not).
:-op(700,xfx,assigned).  % used in simplification. A safe 'is' operator.
:-op(700,xfy,['<=','<', '>', '>=', '<>', '==', '!=']).
:-op(200,xfy,'**').
:-op(200,xfy, in).  % used in quants.

% uses path in .plrc
:- ensure_loaded([  % lib('input.prolog') for getText(Text)?, loads ctypes
		  lib(output), % indent(N), newline, writeString
                  lib(equtaut), lib(simp),
                  lib(clean), % to clean up C 
		  lib(charsio), qlib(qlists)]).

:-op(100, fx, '&').  % used in symbex for procedure args.

% C-operators for symbex and wp.

:-op(100, xf,['++', '--']).
:-op(100, fx, ['++', '--']).
:-op(100, xfy, ['+=', '-=', '*=', '/=']).
:-op(601, xfy, ':').
:-op(602, xfy, '?').

% =========================================================================

activate :- write('Version 5ASWI'), nl,
	getTheories,
        (exists_file('simplification.rules'),
               theory('simplification.rules'); true),
	readCode(C), !, program(C), 
        nl, halt.
%     ;
%	error('Something wrong.').

% read lines of code and concatenate into Code.
readCode(Code) :-
        get_line(Line, Terminator),
       (
        is_endfile(Terminator), Code = Line
        ;
        readCode(More), append(Line,More, Code)
       ).   

testInput2("if(b) x = y+2; if(!b) x = y + 2; x=y;").
testInput3("//{ true } void swap(X, Y); //{ X = 'old Y' and Y = 'old X'}
x=7; swap(&x, &y);").
testInput4("//{x=a and y=0 and a > 0}
while(x != 0) //{x+y=a}{ x = x-1; y = y+1;}").

program(S0) :- 
	fixComment(S, S0, []),
	contracts(S, S1),
	precond0(P,S1,S2), 
	makefun(P, C, F), !,  % C is true by default
	applyFun(F, C, CC),
	statement(1, CC ! F, NewF, S2, Rest), !,
	statements(1, NewF, Post, Rest, LeftOver), 
	unfun(Post, PostTerm),
	simplify(PostTerm, SimpPost),
	nl, writeCond(SimpPost),
	testContra(SimpPost),
	break(LeftOver, Remains),
        (Remains == [] 
	;
         nl, writeStrings(["// Couldn't parse: ", Remains])
	).

contracts --> break, contract, (contracts ; []) ; [].

opT([OpC | "="], OpT) :- atom_codes(OpT, [OpC]).
	
precond0(P) --> break, precond(P), break.
precond(true) -->  "//", break, [12, 12], break, { nl, writeCond(true) }. 
precond(PTerm) --> "//", break, [12], upto(P, [12]), break,
        {  chars_to_term(P, PTerm)
%	,   nl, writeCond(PTerm) 
        }.
precond(true) --> break, { nl, writeCond(true) }.

goal(N, Cond) --> "//", break, [12], upto(Goal, [12], [12]), !, 
	{ 
	  chars_to_term(Goal, GoalTerm), unfun(Cond, CTerm),
	  simplify(GoalTerm, SimGoal),
	  indent(N), write('// assert: '), write(SimGoal),
	  (
	    simtaut(not(CTerm and SimGoal)),
            indent(N), write('// -- assertion is impossible!'),
	    indent(N), write('// -- current state is '),
%	       pretty(CTerm)
               write(CTerm), nl
           ;  
	   simtaut(CTerm implies SimGoal), 
	    indent(N), write('// -- assertion is verified.'), nl
           ;
	    indent(N), write('//  -- assertion may not be valid.'),
	    indent(N), write('//  -- could not prove '),
%	        pretty(CTerm implies SimGoal)
                write(CTerm implies SimGoal), nl
	  )
	 }, break.

unfun(P ! [], P).    
unfun(P ! F, SPT) :- unfun1(F, Term), simplify(P and Term, SPT).
unfun(Rest or P, SYX) :- unfun(P, Y), unfun(Rest, X), simplify(X or Y, SYX).
unfun(_, _) :- error('Error in unfun.').

unfun1([[R, V]], R=V).
unfun1([[R, V] | Rest], Term and (R=V)) :- unfun1(Rest, Term).
unfun1(_, _) :- error('Error in unfun.').

/*
processAssign(X=V, Args, In, Pin, Pin,  Out) :-
        memberchk(&X, Args),
        symex(In, X, V, Out).
processAssign(Rest and (X=V), Args, In, Pin, Pin, Out) :-
        memberchk(&X, Args),
        symex(In, X, V, Out1),
        processAssign(Rest, Args, Out1, Pin, Pin, Out).
processAssign(T, _, In, Pin, Pin and T, In).
*/

assignDummy(X, Args, In, V, Out, InList, [DummyX | InList]) :-
        memberchk(&X, Args),
        name(X,XStr), name('$', [Dollar]), name(DummyX, [Dollar|XStr]),
        symex(In, DummyX, V, Out).

processAssign1(X=V, Args, In, Pin, Pin,  Out, InList, OutList) :-
        assignDummy(X, Args, In, V, Out, InList, OutList).

processAssign1(Rest and (X=V), Args, In, Pin, Pin, Out, InList, OutList) :-
        assignDummy(X, Args, In, V, Out1, InList, NewList),
        processAssign1(Rest, Args, Out1, Pin, Pin, Out, NewList, OutList).

unassignDummy(X, In, Out) :-
        name('$', [Dollar]), name(X, [Dollar|XStr]), name(UnDollar, XStr),
        symex(In, UnDollar, X, Out).
processAssign1(T, _, In, Pin, Pin and T, In).

deleteDollar([], In, In).
deleteDollar([[X, _] | Rest], In, Out) :-
        name('$', [Dollar]), name(X, [Dollar|_]),
        deleteDollar(Rest, In, Out).
deleteDollar([[X, Y] | Rest], In, Out) :-
        deleteDollar(Rest, [[X, Y] | In], Out).

processAssign2([], P ! In, P ! Cleaned) :- deleteDollar(In, [], Cleaned).
processAssign2([X | List], In, Out) :-
        unassignDummy(X, In, New),
        processAssign2(List, New, Out).

processAssign(T, Args, In, Pin, Pout, Out) :-
        processAssign1(T, Args, In, Pin, Pout, New, [], OutList),
        processAssign2(OutList, New, Out).

processPostCon(Rest and T, In, Out) :-
       combine(In, T, Out1),
       processPostCon(Rest, Out1, Out).   
processPostCon(P, In, Out) :-
       combine(In, P, Out).

processPostCon(P, Args, In, Out) :-
	processAssign(P, Args, In, true, Pout, Out1),
	processPostCon(Pout, Out1, Out).

statements(N, Pre, Post)  --> 
	statement(N, Pre, PP), 
	statements(N, PP, Post).
statements(_, Pre, Pre) --> [].

statement(N, Pre, Pre) --> goal(N, Pre), break.
statement(N, Pre, Pre) --> 
	";", break,
	{indent(N), write(';')}.
statement(N, Pre, Post) --> 
	matchP("{", "}", Balanced),
	{ 
	  indent(N), write('{ '),
          statements(N, Pre, Post, Balanced, []),
          indent(N), write(' }')
	}, 
	break.

statement(N, Pre, IfPost or ElsePost) -->
                ifThen(N, Pre, BTerm, IfPre), break,
                statement(N+1, IfPre, IfPost), break,
                elseClause(N, Pre, BTerm, ElsePost), break.

statement(N, Pre, Post) -->
        "while", break, matchP("(", ")", B), break, !,
        { indent(N), writeStrings(["while (", B, ") "]),
          string_to_term(B, BTerm),
          combine(Pre, BTerm, Entry) },
        assertion(Inv), 
       {string_to_term(Inv, InvTerm), 
        unfun(Entry, EntryP),
        (
         simtaut(EntryP implies InvTerm)
        ;
         indent(N+1), 
	 write('Cannot prove that the invariant holds at loop entry.')
        )
       },
	statement(N+1, Entry, Exit),
       {unfun(Exit, ExitP),
        (simtaut(ExitP implies InvTerm)
        ;
         indent(N+1),
         write('Cannot prove that the invariant holds at loop exit.')
        ),
        combine(Pre, InvTerm and not BTerm, Post)
       }.
                    
statement(N, Cond, NewCond) -->
	 "switch", break, matchP("(", ")", Var), break,
	{indent(N), writeStrings(["switch (", Var, ") {"])},
	 matchP("{", "}", Cases), break,
	{ cases(N, Cond, NewCond, Var, Cases, [])}, break.

statement(N, Cond, NewCond) -->
         opAssign(Ref, Val, OpAssign),
        { 
	 opT(OpAssign, OpT),   
	 atom_codes(OpT, OpString),
	 indent(N),
	 writeStrings([Ref, " = ", Ref, OpString, Val, " ;"]),
         chars_to_term(Ref, R), string_to_term(Val, V),
         RHS =.. [OpT, R, V],  
         symex(Cond, R, RHS, NewCond), !
	}, 
	break.
statement(N, Cond, NewCond) -->
        upto(Ref, "=", ";"), upto(Val, ";"),
        { 
	 indent(N), writeStrings([Ref, " = ", Val, " ;"]),
         chars_to_term(Ref, R), string_to_term(Val, V),
         symex(Cond, R, V, NewCond), !
	}, 
	break.            
statement(N, Cond, NewCond) -->
	incdec(Ref, Op), break,
	{ 
          indent(N), writeStrings([Ref, " = ", Ref, " ", [Op], " 1;"]),
          chars_to_term(Ref, R), atom_chars(OpT, [Op]),
	  RHS =.. [OpT, R, 1],
	  symex(Cond, R, RHS, NewCond), !
         }.
statement(N, Pre, Post) -->
	upto(Call,  ";", ";"), break,
	{ doCall(N, Pre, Call, Post), !}.


cases(N, PreCases, PostCases, V) -->
	"case ", break, upto(Case, ":", ":"), break,
	{
         indent(N+1), writeStrings(["case: ", Case]),
         append([V," == ", Case], B),
         string_to_term(B, BTerm),
         combine(PreCases, BTerm, PreCase), unfun(PreCase, UPreCase),
	 writeCond(UPreCase)
	 },
	 caseStatements(N+1, PreCase, PostCase), break,
	 cases(N, PreCases, PostCases, V)
       ;
        "default ", break, ":", break, 
	{ 
	  indent(N+1), write('default :'),
	  unfun(PreCases, UPreCases),
         writeCond(UPreCases) 
	},
	statements(N+1, PreCases, PostCases), 
	("break ", break, ";" , break ; break) % last break optional
       ;
       break.  % default optional.

caseStatements(N, PreCase, PostCase) -->
	"break ", break, ";", break
       ;
        "case ", break, ":", break, caseStatements(N, PreCase, PostCase)
       ;
        statement(N, PreCases, PostCases),
	caseStatements(N,  PreCase, PostCase)
       ;
        break.
                                          
incdec(Ref, Op) -->
	 {memberchk(OpC, ["++", "--"])},
	 upto(Ref, OpC, ";"), break, ";", break,
	 {OpC = [Op, Op]}.
         
doCall(N, Pre, Call, Post) :-
	 indent(N), writeStrings([Call, ";"]),
	 chars_to_term(Call, CallTerm),
         contract(PreCon1, CallTerm, PostCon1), !,
	 cleanPointers(PreCon1, PreCon), cleanPointers(PostCon1, PostCon),
	 unfun(Pre, PreProp),
	 simplify(PreProp implies PreCon, SimpCon), 
	 ( 
	  tautology(SimpCon)
	 ; 
	  indent(N), write( '... cannot show '), 
%	  pretty(SimpCon), 
          write(SimpCon),
	  write(' for '),
	  write(CallTerm), write('.')
	 ),
	  CallTerm =.. [_ | Args],
	  processPostCon(PostCon, Args, Pre, Post).

elseClause(N, Pre, BTerm, Post) --> 
	"else", break,
	{ indent(N), write('else '),
	  combine(Pre, not BTerm, EP), unfun(EP, UEP),
	  simplify(UEP, SUEP), writeCond(SUEP),
	  checkCond(N, Pre, SUEP),
	  !},
	statement(N+1, EP, Post).
elseClause(_, Pre, BTerm, Post) --> 
	{ combine(Pre, not BTerm, Post), !}.

ifThen(Indent, Pre, BTerm, IfP) --> 
	"if", break, matchP("(", ")", B), break,
        { indent(Indent), writeStrings(["if (", B, ") "]),
	  string_to_term(B, BTerm),
          combine(Pre, BTerm,IfP), unfun(IfP, UIfP),
	  simplify(UIfP, SUIfP), writeCond(SUIfP),
	  checkCond(Indent, Pre, SUIfP),
	  ! }.

opAssign(Ref, Val, OpAssign) -->
	{ member(OpAssign, ["+=", "*=", "/=", "&=", "-=", "|="])},
        upto(Ref, OpAssign, ";"),  upto(Val, ";", ";").

checkCond(Indent, Pre, C) :- unfun(Pre, UPre), 
     ( simtaut(UPre implies C) ->
	indent(Indent), write('// This branch is always taken.')
     ;
       simtaut(UPre implies not C) ->  
        indent(Indent), write('// This branch is never taken.')
     ;
      true
     ).

pretty(P) :- pretty(P, 72).

writeCond(P) :- write('//{ '), writeC(P), write(' }').
% writeC(P ! []) :- pretty(P).
writeC(P ! []) :- write(P).
% writeC(P ! F) :- pretty(P), write(' and '), writeF(F).
writeC(P ! F) :- write(P), write(' and '), writeF(F).
writeC((P ! F) or Rest) :- 
	write('( '), writeC(P ! F), write(' )'), write(' or '), writeC(Rest).
% writeC(P) :- pretty(P).
writeC(P) :- write(P).

combine(P ! F, B, S ! F) :- 
	applyFun(F, B, Result), simplify(P and Result, S).
combine(Rest or (P ! F), B, RestP or S) :-
	combine(P ! F, B, S),
	combine(Rest, B, RestP).
combine(_,_,_) :- error('!! Error in combine procedure.').


symex(P ! F, R, V, NewCond) :-
          \+ member([R, _], F),
	     applyInitial1(R, V, ModifiedV),
	     applyInitial1(R, P, ModifiedP),
	     applyInitial(R, F, ModifiedF),
	     symex0(ModifiedP ! ModifiedF, R, ModifiedV, NewCond)
	 ; 
             symex0(P ! F, R, V, NewCond).

symex(X, R, V, N) :-
        symex0(X, R, V, N)
	;
        error('Bug in symex.').
        
symex0(P ! F, R, V, NewP ! NewF) :- symex1(P ! F, R, V, NewP ! NewF).
symex0(Rest or (P ! F), R, V, Result or (NewP ! NewF)) :-
        symex(P ! F, R, V, NewP ! NewF), symex(Rest, R, V, Result).
symex0(Branch1 or Branch2, R, V, Result1 or Result2) :-
	symex(Branch1, R, V, Result1), symex(Branch2, R, V, Result2).
symex1(P ! F, R, V, NewP ! NewF) :-
        applyFun(F, V, NewV),
        simplify(NewV, SimV),
        update(F, R, SimV, NewF),
        applyFun(NewF, P, NewP).

applyInitial1(V, Expr, Result) :-
        path_arg(Path, Expr, V), makeOld(V, OldV),
        change_path_arg(Path, Expr, Modified, OldV),
        !,
        applyInitial1(V, Modified, Result).
applyInitial1(_, Expr, Expr).   

makeOld(V, OldV) :-
        atom_codes(V, Vstr), 
       (
        append("old", _, Vstr), OldV = V
       ;
	append("old ", Vstr, OldVstr),
        atom_codes(OldV, OldVstr)
       ).


applyInitial(_, [], []).
applyInitial(Initial, [[Z, Expr] | Rest], [[Z, Applied] | AppliedRest]) :-
        applyInitial1(Initial, Expr, Applied),
        applyInitial(Initial, Rest, AppliedRest).


% based on Quintus Prolog Library Manual, p. 40
applyFun(Function, Expr, Final) :-
        path_arg(Path, Expr, Lhs), 
	(
	 Lhs = 'OLD'(A), 
	 ( memberchk([A, E], Function) -> Rhs = E
	  ;
	   makeOld(A, Rhs)
         )
	;
	 atom(Lhs), memberchk([Lhs, Rhs], Function)
	),
        change_path_arg(Path, Expr, Modified, Rhs),
        !,
        applyFun(Function, Modified, Final).
applyFun( _, Expr, Expr).

update(F, R, NewV, NewF) :-
	change_path_arg(_, F, [R, _], NewF, [R, NewV])
	;
	append([[R, NewV]], F, NewF).

writefun([]).
writefun(F) :- write('{ '), writeF(F), write(' }').
writeF([[R,V] | Rest]) :-  write(R = V), writeF1(Rest).
writeF1([]).
writeF1([[R, V] | Rest]) :- write(' and '), write(R = V), writeF1(Rest).
/*
makefun(X=Y, C, [[X,Y]]) :- 
	atom(X), 
	(
	 free_of_term(X,Y), 
	 (var(C) -> C = true ; true)
	; 
	 error('Something wrong in the initial condition.')
	).
makefun(Rest and X=Y, C, [[X,Y] | RestF]) :- atom(X), makefun(Rest, C, RestF).
makefun(F and C, C, FList) :- makefun(F, C, FList).
makefun(C, C, []) :- var(C) -> C=true ; true.
makefun(_,_,_) :- error('Something wrong in the initial condition.').
*/
% makefun(InCon, OutCon, Flist)
makefun(C, C, []) :- var(C) -> C=true.
makefun(X=Y, C, [[X,Y]]) :-
        atom(X),
        (
         free_of_term(X,Y),
         (var(C) -> C = true ; true)
        ).

makefun(Rest and X=Y, C, [[X,Y] | RestF]) :- atom(X), makefun(Rest, C, RestF).
makefun(F and C,NewC and C, FList) :- makefun(F, NewC, FList).
makefun(C, C, []).
makefun(_,_,_) :- error('Something wrong in the initial condition.').    

contract -->
	assertion(Pre),
	proc(Call),
	assertion(Post),
      { nl, nl,
        append(["contract(", Pre, ",",  Call, ",", Post, ")"], ContractString),
	mapOld(ContractString, Contract),
	chars_to_term(Contract, ContractTerm),
	assertz(ContractTerm)
       }.

mapOld(Old, New) :-
        mapOld1(Prefix, NewSubstring, Old, Rest),
        mapOld(Rest, NewRest),
        append([Prefix, NewSubstring, NewRest], New).
mapOld(Old, Old).


mapOld1(Prefix, New) --> 
	upto(Prefix, "'","'"),
	"old ", upto(Var, "'", "'"),
	{append(["'OLD'(", Var, ")"], New)}.

unmapOld(Term, New) :-
	path_arg(Path, Term, 'OLD'(X)),
	atom_codes(X, Name),
	append("old ", Name, OldName),
	atom_chars(Atom, OldName),
        change_path_arg(Path, Term, Modified, Atom),
        !,
        unmapOld(Modified, New).   
unmapOld(Term, Term).

assertion(P) --> "//", break, [12], upto(P, [12], ";"), break,
	{nl, writeStrings(["//{ ", P, " }"]), !}.
 
proc(Call) -->
	"void ", upto(Call, ";", ";"), break,
	{nl, writeStrings(["void ", Call, ";"]), !}.

cleanPointers(Expr, Final) :-
        path_arg(Path, Expr, &X),
        change_path_arg(Path, Expr, Modified, X),
        !,
        cleanPointers(Modified, Final).
cleanPointers(Expr, Expr).                 

testContra(Prop) :-
	simtaut(not(Prop)) ->
	  nl, write('The final state is a contradiction.'), nl
       ;
        true.

simtaut(T) :- simplify(T, ST), !, tautology(ST).












