001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: package de.uka.ilkd.key.proof.init;
011:
012: import java.util.Enumeration;
013: import java.util.LinkedList;
014: import java.util.Vector;
015:
016: import de.uka.ilkd.key.java.*;
017: import de.uka.ilkd.key.java.expression.Literal;
018: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
019: import de.uka.ilkd.key.java.reference.ExecutionContext;
020: import de.uka.ilkd.key.java.reference.FieldReference;
021: import de.uka.ilkd.key.java.statement.MethodFrame;
022: import de.uka.ilkd.key.java.statement.SynchronizedBlock;
023: import de.uka.ilkd.key.java.visitor.CreatingASTVisitor;
024: import de.uka.ilkd.key.logic.*;
025: import de.uka.ilkd.key.logic.op.*;
026: import de.uka.ilkd.key.logic.sort.Sort;
027: import de.uka.ilkd.key.proof.*;
028: import de.uka.ilkd.key.proof.mgt.Contract;
029: import de.uka.ilkd.key.proof.mgt.Contractable;
030: import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
031: import de.uka.ilkd.key.rule.TacletApp;
032: import de.uka.ilkd.key.util.ExtList;
033: import de.uka.ilkd.key.util.KeYExceptionHandler;
034:
035: /* TODO
036:
037: synchro:
038: -(X)convert MetaClassReference to a constant
039: -skip 1st statement in block
040:
041: sequent state:
042: -extend to qualif. attributes and arrays as lvalues
043:
044: syntactic cond.:
045: -(X)add a semantic check at "leaf" nodes
046: -generalize set elements from SV to schematic terms
047:
048: jmm stuff:
049: -rename variables
050: -(-)generalize constants
051: -volatile variables
052: */
053:
054: public class NonInterferencePO implements ProofOblInput {
055:
056: ProofAggregate po;
057: InitConfig initConfig;
058: Proof proof1, proof2;
059:
060: ProgramVariable trueSelf;
061:
062: public NonInterferencePO(ProofEnvironment env, Proof p1, Proof p2) {
063: initConfig = env.getInitConfig();
064: if (p1 == null || p2 == null)
065: throw new IllegalStateException(
066: "Proofs are not initialised");
067: proof1 = p1;
068: proof2 = p2;
069: trueSelf = (ProgramVariable) proof1.getNamespaces()
070: .programVariables().lookup(new Name("self"));
071: }
072:
073: public ProofAggregate getPO() {
074: return po;
075: }
076:
077: public void readProblem(ModStrategy mod) throws ProofInputException {
078: Proof p = new Proof(
079: name(), // just a dummy, see createSubgoals()
080: TermFactory.DEFAULT.createJunctorTerm(Op.FALSE),
081: "HOLA!", initConfig.createTacletIndex(), initConfig
082: .createBuiltInRuleIndex(), initConfig
083: .getServices());
084:
085: po = ProofAggregate.createProofAggregate(new Proof[] { p },
086: name());
087:
088: }
089:
090: public void createSubgoals() {
091: Proof p = po.getFirstProof();
092:
093: Vector nodes1 = new Vector();
094: Vector nodes2 = new Vector();
095: getSymExecNodes(proof1.root(), false, nodes1);
096: getSymExecNodes(proof2.root(), true, nodes2);
097:
098: LinkedList conditions = new LinkedList();
099:
100: //create the crossproduct of the two lists
101: for (Enumeration i = nodes1.elements(); i.hasMoreElements();) {
102: Node a = (Node) i.nextElement();
103: for (Enumeration j = nodes2.elements(); j.hasMoreElements();) {
104: Node b = (Node) j.nextElement();
105: if (syntacticNonInterference(a, b))
106: continue;
107: ConstrainedFormula cf = new ConstrainedFormula(
108: nonInterfCondition(a, b));
109: conditions.addFirst(new ConditionContainer(cf, a
110: .serialNr()
111: + "<->" + b.serialNr()));
112: }
113: }
114:
115: Goal firstGoal = p.openGoals().head();
116: ListOfGoal newGoals = firstGoal.split(conditions.size());
117: de.uka.ilkd.key.proof.IteratorOfGoal it = newGoals.iterator();
118: while (it.hasNext()) {
119: Goal g = it.next();
120: ConditionContainer cc = (ConditionContainer) conditions
121: .getFirst();
122: g.addFormula(cc.getFormula(), false, false);
123: g.setBranchLabel(cc.getLabel());
124: conditions.removeFirst();
125: }
126:
127: p.replace(firstGoal, newGoals);
128: }
129:
130: /** Serves as an utility-method for getPOTerm(). It takes a Node
131: (from a proof), traverses the tree of nodes, and collects in v all
132: nodes where symbolic execution has been performed. To reduce the
133: number of collected elements only nodes with updates will be
134: collected if the parameter onlyUpdates is true. */
135: private void getSymExecNodes(Node n, boolean onlyUpdates, Vector v) {
136: if (v == null)
137: throw new IllegalStateException(
138: "The second parameter of getSMNodes is not initialised");
139: if (n == null)
140: return;
141: if (n.getNodeInfo().getActiveStatement() != null) {
142: /*This is the case if symbolic modification has been performed*/
143: if (onlyUpdates) {
144: String ruleName = n.getAppliedRuleApp().rule().name()
145: .toString();
146: if (ruleName.startsWith("assignment_"))
147: v.add(n);
148: } else {
149: v.add(n);
150: }
151: }
152: for (IteratorOfNode ni = n.childrenIterator(); ni.hasNext();) {
153: getSymExecNodes(ni.next(), onlyUpdates, v);
154: }
155: }
156:
157: /**
158: Serves the getPOTerm() method.
159: @param a gamma1,gamma2,..., gammaN => <p1> phi
160: @param b delta1,delta2,..., deltaM => <p2> psi
161: @return gamma1,gamma2,...,gammaN,delta1,delta2,...,deltaM => <p2'> gamma1,gamma2,...,gammaN
162: where p2' is the first assignment statement of p2.
163: */
164: private Term nonInterfCondition(Node a, Node b) {
165: Sequent sa = a.sequent();
166: Sequent sb = b.sequent();
167:
168: Term stateA = sequentState(sa);
169: Term resAnte = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
170: stateA, sequentState(sb));
171:
172: JavaProgramElement progA = program(sa);
173: JavaProgramElement progB = program(sb);
174:
175: Term sc = syncCondition(progA, progB);
176: if (sc != null) {
177: resAnte = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
178: resAnte, sc);
179: }
180:
181: FirstStatementExtractionVisitor v = new FirstStatementExtractionVisitor(
182: progB, b);
183: v.start();
184: JavaBlock p2prime = JavaBlock
185: .createJavaBlock((StatementBlock) v.result());
186: Term resSucc = TermFactory.DEFAULT.createBoxTerm(p2prime,
187: stateA);
188:
189: return TermFactory.DEFAULT.createJunctorTerm(Op.IMP, resAnte,
190: resSucc);
191: }
192:
193: private JavaProgramElement program(Sequent s) {
194: Term formula = s.succedent().getFirst().formula();
195: while (formula.op() instanceof IUpdateOperator) {
196: // skip update
197: formula = ((IUpdateOperator) formula.op()).target(formula);
198: }
199: if (formula.op() != Op.DIA)
200: throw new IllegalStateException(
201: "Diamondoperator expected at top of " + formula
202: + " in " + s);
203: return formula.javaBlock().program();
204: }
205:
206: static int varNr = 0;
207:
208: private Term sequentState(Sequent s) {
209: Term progTerm = s.succedent().getFirst().formula();
210: Term result = null;
211:
212: Term gamma = TermFactory.DEFAULT.createJunctorTerm(Op.TRUE);
213: for (IteratorOfConstrainedFormula icf = s.antecedent()
214: .iterator(); icf.hasNext();) {
215: gamma = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
216: gamma, icf.next().formula());
217: }
218:
219: if (progTerm.op() instanceof IUpdateOperator) {
220: // TODO: what to change for quantified updates here??? /PR
221:
222: IUpdateOperator upOp = (IUpdateOperator) progTerm.op();
223:
224: int nrUps = upOp.locationCount(); // number of updates
225:
226: Term[] locs = new Term[nrUps];
227: Term[] values = new Term[nrUps];
228: Term target = gamma;
229: for (int k = 0; k < nrUps; k = k + 1) { //fix update with new vars
230: locs[k] = upOp.location(progTerm, k);
231: LogicVariable newVar = new LogicVariable(new Name(
232: "neww" + varNr++), upOp.value(progTerm, k)
233: .sort());
234: values[k] = TermFactory.DEFAULT
235: .createVariableTerm(newVar);
236: }
237: result = TermFactory.DEFAULT.createUpdateTerm(locs, values,
238: target); // apply update to gamma
239:
240: for (int k = 0; k < nrUps; k++) { // add equations for "new" values
241: // XXX: here more work has to be done if x is more complex
242: Term left = locs[k];
243: target = upOp.value(progTerm, k);
244: Term right = TermFactory.DEFAULT.createUpdateTerm(locs,
245: values, target);
246: Term updEqTerm = TermFactory.DEFAULT
247: .createEqualityTerm(left, right);
248: result = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
249: result, updEqTerm);
250: }
251:
252: for (int k = 0; k < nrUps; k++) { // quantify existentially
253: result = TermFactory.DEFAULT.createQuantifierTerm(
254: Op.EX, (LogicVariable) values[k].op(), result);
255: }
256:
257: } else
258: result = gamma;
259:
260: return result;
261: }
262:
263: int nr = 0;
264:
265: public boolean syntacticNonInterference(Node a, Node b) {
266:
267: System.err.println(nr++);
268: //get TacletApp for Instantiations
269: TacletApp tapp1 = (TacletApp) a.getAppliedRuleApp();
270: TacletApp tapp2 = (TacletApp) b.getAppliedRuleApp();
271: if ("empty_modality".equals(tapp1.rule().name().toString()))
272: return false;
273:
274: //get Read-Sets
275: ListOfSchemaVariable readVars1 = tapp1.taclet().readSet();
276: ListOfSchemaVariable readVars2 = tapp2.taclet().readSet();
277: ListOfSchemaVariable writeVars1 = tapp1.taclet().writeSet();
278: ListOfSchemaVariable writeVars2 = tapp2.taclet().writeSet();
279:
280: if (hasIntersection(instantiate(readVars1, tapp1), instantiate(
281: writeVars2, tapp2)))
282: return false;
283: if (hasIntersection(instantiate(readVars2, tapp2), instantiate(
284: writeVars1, tapp1)))
285: return false;
286: if (hasIntersection(instantiate(writeVars1, tapp1),
287: instantiate(writeVars2, tapp2)))
288: return false;
289:
290: return true;
291: }
292:
293: private Vector instantiate(ListOfSchemaVariable vlist,
294: TacletApp tapp) {
295: //System.err.print(vlist+"->");
296: Vector result = new Vector(5);
297: IteratorOfSchemaVariable vit = vlist.iterator();
298: while (vit.hasNext()) {
299: Object inst = tapp.instantiations().getInstantiation(
300: vit.next());
301: if (inst instanceof Literal)
302: continue;
303: if (inst instanceof ProgramVariable)
304: continue;
305: if ((inst instanceof FieldReference)
306: && (((FieldReference) inst).getProgramVariable()
307: .isImplicit()))
308: continue;
309: result.add(inst);
310: }
311: //System.err.println(result);
312: return result;
313:
314: }
315:
316: public void setExceptionHandler(KeYExceptionHandler keh) {
317: }
318:
319: private boolean hasIntersection(Vector l1, Vector l2) {
320: for (Enumeration i = l1.elements(); i.hasMoreElements();) {
321: Sort s = getSort(i.nextElement());
322: for (Enumeration j = l2.elements(); j.hasMoreElements();)
323: if (checkCompatibility(s, getSort(j.nextElement())))
324: return true;
325: }
326: return false;
327:
328: }
329:
330: public Sort getSort(Object var) {
331: if (var == null)
332: return null;
333: Sort s = null;
334: de.uka.ilkd.key.java.abstraction.KeYJavaType kjt = null;
335: if (var instanceof FieldReference)
336: kjt = ((FieldReference) var).getKeYJavaType();
337: if (var instanceof ProgramVariable)
338: kjt = ((ProgramVariable) var).getKeYJavaType();
339: if ((var != null) && (kjt == null))
340: System.err.println("NULL KJT OF " + var + " "
341: + var.getClass() + " " + kjt);
342: s = kjt.getSort();
343: if ((var != null) && (s == null))
344: System.err.println("NULL SORT OF " + var + " "
345: + var.getClass() + " " + kjt);
346: return s;
347: }
348:
349: public boolean checkCompatibility(Sort s1, Sort s2) {
350: if (s1 == null || s2 == null)
351: return false;
352: return (s1.extendsTrans(s2) || (s2.extendsTrans(s1)));
353: }
354:
355: private Term syncCondition(JavaProgramElement pa,
356: JavaProgramElement pb) {
357: Term exa = syncExpr(pa);
358: Term exb = syncExpr(pb);
359: if ((exa == null) || (exb == null))
360: return null;
361: Term result = TermFactory.DEFAULT.createJunctorTerm(Op.EQUALS,
362: exa, exb);
363: result = TermFactory.DEFAULT.createJunctorTerm(Op.NOT, result);
364: return result;
365: }
366:
367: public Term syncExpr(JavaProgramElement pp) {
368: Expression syncExpr = null;
369: ExecutionContext ec = null;
370: SourceElement p = pp;
371: while (true) {
372: if (p instanceof SynchronizedBlock) {
373: syncExpr = ((SynchronizedBlock) p).getExpression();
374: } else if (p instanceof MethodFrame) {
375: ec = (ExecutionContext) ((MethodFrame) p)
376: .getExecutionContext();
377: } else if (!(p instanceof ProgramPrefix)) {
378: break;
379: }
380: SourceElement pnext = p.getFirstElement();
381: if (p == pnext) {
382: break;
383: } else {
384: p = pnext;
385: }
386: }
387: if (syncExpr == null) {
388: return null;
389: } else {
390: return initConfig.getServices().getTypeConverter()
391: .convertToLogicElement(syncExpr, ec);
392: }
393: }
394:
395: public boolean askUserForEnvironment() {
396: return true;
397: }
398:
399: /** returns the path to the Java model.
400: */
401: public String getJavaPath() throws ProofInputException {
402: return null;
403: }
404:
405: /** set the initial configuration used to read an input. It may become
406: * modified during reading depending on the modification strategy used
407: * for reading.
408: */
409: public void setInitConfig(InitConfig i) {
410: }
411:
412: public void readSpecs() {
413: }
414:
415: public void readActivatedChoices() throws ProofInputException {
416: //nothing to do
417: }
418:
419: public SetOfChoice getActivatedChoices() throws ProofInputException {
420: return null;
421:
422: }
423:
424: /** reads the include section and returns an Includes object.
425: */
426: public Includes readIncludes() throws ProofInputException {
427: return new Includes();
428: }
429:
430: /** returns the name of the proof obligation input.
431: */
432: public String name() {
433: return "Non-Interference of ... and ...";
434: }
435:
436: public Contractable[] getObjectOfContract() {
437: return new Contractable[0];
438: }
439:
440: public boolean initContract(Contract ct) {
441: return false;
442: }
443:
444: public void startProtocol() {
445: // do nothing
446: }
447:
448: private class FirstStatementExtractionVisitor extends
449: CreatingASTVisitor {
450:
451: private ProgramElement result;
452: private Node node;
453:
454: public FirstStatementExtractionVisitor(ProgramElement root,
455: Node n) {
456: super (root, true);
457: this .node = n;
458: }
459:
460: /** starts the walker*/
461: public void start() {
462: stack.push(new ExtList());
463: walk(root());
464: ExtList el = stack.peek();
465: int i = 0;
466: while (!(el.get(i) instanceof ProgramElement)) {
467: i++;
468: }
469: result = (ProgramElement) (stack.peek()).get(i);
470: }
471:
472: public ProgramElement result() {
473: return result;
474: }
475:
476: public void performActionOnStatementBlock(StatementBlock x) {
477: StatementBlock newBlock = x;
478: ExtList changeList = stack.peek();
479: if (changeList.getFirst() == CHANGED) { //process change in children
480: changeList.removeFirst();
481: newBlock = new StatementBlock(changeList);
482: }
483:
484: if (newBlock.getStatementCount() > 1) {
485: addChild(new StatementBlock((Statement) newBlock
486: .getFirstElement()));
487: changed();
488: } else {
489: doDefaultAction(newBlock);
490: changed(); // in case of immediately nested blocks
491: }
492: }
493:
494: public void performActionOnIntLiteral(IntLiteral x) {
495: ProgramVariable pv = new LocationVariable(
496: new ProgramElementName("some_int"), x
497: .getKeYJavaType(initConfig.getServices()));
498: // node.setGlobalProgVars(getGlobalProgVars().add(pv));
499: addChild(pv);
500: changed();
501: }
502:
503: }
504:
505: private class ConditionContainer {
506: private ConstrainedFormula f;
507: private String label;
508:
509: public ConditionContainer(ConstrainedFormula f, String s) {
510: this .f = f;
511: this .label = s;
512: }
513:
514: public ConstrainedFormula getFormula() {
515: return f;
516: }
517:
518: public String getLabel() {
519: return label;
520: }
521: }
522:
523: }
|