From 2bf9425fe2b844c53ecbe54d616d86a2c6d0c6a8 Mon Sep 17 00:00:00 2001 From: Benjamin Weiss Date: Mon, 22 Dec 2008 10:13:26 +0100 Subject: [PATCH] graceful handling of unsupported JML features (issue #930) --- system/Makefile | 3 +- .../key/java/recoderext/JMLTransformer.java | 42 ++- .../ilkd/key/speclang/PositionedString.java | 2 +- .../de/uka/ilkd/key/speclang/SLEnvInput.java | 76 +++++ .../uka/ilkd/key/speclang/SpecExtractor.java | 7 + .../key/speclang/jml/JMLSpecExtractor.java | 320 +++++++++--------- .../jml/pretranslation/jmlpreparser.g | 40 ++- .../jml/translation/JMLSpecFactory.java | 4 +- .../key/speclang/jml/translation/jmlparser.g | 48 +-- .../key/speclang/ocl/OCLSpecExtractor.java | 15 +- .../SLTranslationExceptionManager.java | 23 +- .../translation/SLWarningException.java | 32 ++ 12 files changed, 369 insertions(+), 243 deletions(-) create mode 100644 system/de/uka/ilkd/key/speclang/translation/SLWarningException.java diff --git a/system/Makefile b/system/Makefile index 75500c732db..966726cf14c 100644 --- a/system/Makefile +++ b/system/Makefile @@ -257,7 +257,8 @@ GENERATED_SETS=logic/SetAsListOfTerm collection/SetAsListOfString \ java/statement/SetAsListOfLoopStatement \ proof/SetAsListOfGoalChooserBuilder \ strategy/SetAsListOfStrategyFactory \ - logic/op/SetAsListOfLocation + logic/op/SetAsListOfLocation \ + speclang/SetAsListOfPositionedString GENERATED_MAPS= collection/MapAsListFromIntegerToString \ logic/op/MapAsListFromQuantifiableVariableToInteger \ diff --git a/system/de/uka/ilkd/key/java/recoderext/JMLTransformer.java b/system/de/uka/ilkd/key/java/recoderext/JMLTransformer.java index 6e606f04274..07dc39be370 100644 --- a/system/de/uka/ilkd/key/java/recoderext/JMLTransformer.java +++ b/system/de/uka/ilkd/key/java/recoderext/JMLTransformer.java @@ -18,12 +18,9 @@ import de.uka.ilkd.key.collection.SLListOfString; import de.uka.ilkd.key.gui.configuration.ProofSettings; import de.uka.ilkd.key.speclang.PositionedString; -import de.uka.ilkd.key.speclang.jml.pretranslation.KeYJMLPreParser; -import de.uka.ilkd.key.speclang.jml.pretranslation.ListOfTextualJMLConstruct; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLFieldDecl; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSetStatement; +import de.uka.ilkd.key.speclang.SetAsListOfPositionedString; +import de.uka.ilkd.key.speclang.SetOfPositionedString; +import de.uka.ilkd.key.speclang.jml.pretranslation.*; import de.uka.ilkd.key.speclang.translation.SLTranslationException; import recoder.CrossReferenceServiceConfiguration; import recoder.abstraction.Constructor; @@ -47,6 +44,8 @@ public class JMLTransformer extends RecoderModelTransformer { "public", "static"}); + private static SetOfPositionedString warnings; + /** * Creates a transformation that adds JML specific elements, for example @@ -64,13 +63,14 @@ public class JMLTransformer extends RecoderModelTransformer { public JMLTransformer(CrossReferenceServiceConfiguration services, TransformerCache cache) { super(services, cache); + warnings = SetAsListOfPositionedString.EMPTY_SET; } - // ------------------------------------------------------------------------- - // private helper methods - // ------------------------------------------------------------------------- + //------------------------------------------------------------------------- + //private helper methods + //------------------------------------------------------------------------- /** * Concatenates the passed comments in a position-preserving way. @@ -204,9 +204,9 @@ private Comment[] getCommentsAndSetParent(ProgramElement pe) { - // ------------------------------------------------------------------------- - // private transformation methods - // ------------------------------------------------------------------------- + //------------------------------------------------------------------------- + //private transformation methods + //------------------------------------------------------------------------- private void transformFieldDecl(TextualJMLFieldDecl decl, Comment[] originalComments) @@ -416,6 +416,7 @@ private void transformClasslevelComments(TypeDeclaration td, = new KeYJMLPreParser(concatenatedComment, fileName, pos); ListOfTextualJMLConstruct constructs = preParser.parseClasslevelComment(); + warnings = warnings.union(preParser.getWarnings()); //handle model and ghost declarations in textual constructs //(and set assignments which RecodeR evilly left hanging *behind* @@ -475,6 +476,7 @@ private void transformMethodlevelCommentsHelper(ProgramElement pe, = new KeYJMLPreParser(concatenatedComment, fileName, pos); ListOfTextualJMLConstruct constructs = preParser.parseMethodlevelComment(); + warnings = warnings.union(preParser.getWarnings()); //handle ghost declarations and set assignments in textual constructs for(TextualJMLConstruct c : constructs) { @@ -498,9 +500,9 @@ private void transformMethodlevelComments(MethodDeclaration md, - // ------------------------------------------------------------------------- - // RecoderModelTransformer - abstract methods implementation - // ------------------------------------------------------------------------- + //------------------------------------------------------------------------- + //RecoderModelTransformer - abstract methods implementation + //------------------------------------------------------------------------- protected void makeExplicit(TypeDeclaration td) { assert false; @@ -544,6 +546,7 @@ public void makeExplicit() { // use getOriginalDataLocation instead DataLocation dl = unit.getOriginalDataLocation(); String fileName = dl == null ? "" : dl.toString(); + fileName = fileName.replaceFirst("FILE:", ""); transformClasslevelComments(td, fileName); @@ -554,7 +557,7 @@ public void makeExplicit() { ConstructorDeclaration cd = (ConstructorDeclaration) constructorList.get(k); - transformMethodlevelComments(cd, unit.getName()); + transformMethodlevelComments(cd, fileName); } } @@ -564,7 +567,7 @@ public void makeExplicit() { MethodDeclaration md = (MethodDeclaration) methodList.get(k); - transformMethodlevelComments(md, unit.getName()); + transformMethodlevelComments(md, fileName); } } @@ -583,6 +586,11 @@ public void makeExplicit() { } + public static SetOfPositionedString getWarningsOfLastInstance() { + return warnings; + } + + //------------------------------------------------------------------------- //inner classes //------------------------------------------------------------------------- diff --git a/system/de/uka/ilkd/key/speclang/PositionedString.java b/system/de/uka/ilkd/key/speclang/PositionedString.java index 36e797c9d52..e7c818e631a 100644 --- a/system/de/uka/ilkd/key/speclang/PositionedString.java +++ b/system/de/uka/ilkd/key/speclang/PositionedString.java @@ -45,7 +45,7 @@ public PositionedString(String text) { public String toString() { - return text; + return text + " (" + fileName + ", " + pos + ")"; } diff --git a/system/de/uka/ilkd/key/speclang/SLEnvInput.java b/system/de/uka/ilkd/key/speclang/SLEnvInput.java index 30bc3969ea0..771adb3da16 100644 --- a/system/de/uka/ilkd/key/speclang/SLEnvInput.java +++ b/system/de/uka/ilkd/key/speclang/SLEnvInput.java @@ -10,10 +10,19 @@ package de.uka.ilkd.key.speclang; +import java.awt.BorderLayout; +import java.awt.Container; +import java.awt.Dimension; +import java.awt.event.ActionEvent; +import java.awt.event.ActionListener; +import java.awt.event.KeyEvent; import java.util.Arrays; import java.util.Comparator; import java.util.Set; +import javax.swing.*; + +import de.uka.ilkd.key.gui.Main; import de.uka.ilkd.key.gui.configuration.GeneralSettings; import de.uka.ilkd.key.gui.configuration.ProofSettings; import de.uka.ilkd.key.java.JavaInfo; @@ -79,6 +88,67 @@ public int compare(KeYJavaType o1, KeYJavaType o2) { } + private void showWarningDialog(SetOfPositionedString warnings) { + if(!Main.visible) { + return; + } + + final JDialog dialog = new JDialog(Main.getInstance(), + getLanguage() + " warning", + true); + dialog.setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE); + Container pane = dialog.getContentPane(); + pane.setLayout(new BorderLayout()); + + //top label + JLabel label = new JLabel("The following non-fatal " + + "problems occurred when translating your " + + getLanguage() + " specifications:"); + label.setBorder(BorderFactory.createEmptyBorder(5, 5, 0, 5)); + pane.add(label, BorderLayout.NORTH); + + //scrollable warning list + JScrollPane scrollpane = new JScrollPane(); + scrollpane.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5)); + JList list = new JList(warnings.toArray()); + list.setBorder(BorderFactory.createLoweredBevelBorder()); + scrollpane.setViewportView(list); + pane.add(scrollpane, BorderLayout.CENTER); + + //ok button + final JButton button = new JButton("OK"); + button.addActionListener(new ActionListener() { + public void actionPerformed(ActionEvent e) { + dialog.setVisible(false); + dialog.dispose(); + } + }); + Dimension buttonDim = new Dimension(100, 27); + button.setPreferredSize(buttonDim); + button.setMinimumSize(buttonDim); + JPanel panel = new JPanel(); + panel.add(button); + pane.add(panel, BorderLayout.SOUTH); + dialog.getRootPane().setDefaultButton(button); + + button.registerKeyboardAction( + new ActionListener() { + public void actionPerformed(ActionEvent event) { + if(event.getActionCommand().equals("ESC")) { + button.doClick(); + } + } + }, + "ESC", + KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), + JComponent.WHEN_IN_FOCUSED_WINDOW); + + dialog.setSize(700, 300); + dialog.setLocationRelativeTo(Main.getInstance()); + dialog.setVisible(true); + } + + private void createSpecs(SpecExtractor specExtractor) throws ProofInputException { JavaInfo javaInfo @@ -124,6 +194,12 @@ private void createSpecs(SpecExtractor specExtractor) } } } + + //show warnings to user + SetOfPositionedString warnings = specExtractor.getWarnings(); + if(warnings != null && warnings.size() > 0) { + showWarningDialog(warnings); + } } diff --git a/system/de/uka/ilkd/key/speclang/SpecExtractor.java b/system/de/uka/ilkd/key/speclang/SpecExtractor.java index 5a3102e0ddf..02735e60e28 100644 --- a/system/de/uka/ilkd/key/speclang/SpecExtractor.java +++ b/system/de/uka/ilkd/key/speclang/SpecExtractor.java @@ -38,4 +38,11 @@ public SetOfClassInvariant extractClassInvariants(KeYJavaType kjt) public LoopInvariant extractLoopInvariant(ProgramMethod pm, LoopStatement loop) throws SLTranslationException; + + /** + * Returns all warnings generated so far in the translation process. + * (e.g. this may warn about unsupported features which have been ignored + * by the translation) + */ + public SetOfPositionedString getWarnings(); } diff --git a/system/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/system/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java index 75e577b8ac9..d4505db7bfe 100644 --- a/system/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java +++ b/system/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java @@ -18,6 +18,7 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.java.abstraction.Type; import de.uka.ilkd.key.java.declaration.*; +import de.uka.ilkd.key.java.recoderext.JMLTransformer; import de.uka.ilkd.key.java.reference.ArrayOfTypeReference; import de.uka.ilkd.key.java.statement.LoopStatement; import de.uka.ilkd.key.logic.Name; @@ -25,64 +26,50 @@ import de.uka.ilkd.key.logic.op.ProgramMethod; import de.uka.ilkd.key.logic.sort.ArrayOfSort; import de.uka.ilkd.key.logic.sort.Sort; -import de.uka.ilkd.key.speclang.ClassInvariant; -import de.uka.ilkd.key.speclang.LoopInvariant; -import de.uka.ilkd.key.speclang.PositionedString; -import de.uka.ilkd.key.speclang.SetAsListOfClassInvariant; -import de.uka.ilkd.key.speclang.SetAsListOfOperationContract; -import de.uka.ilkd.key.speclang.SetOfClassInvariant; -import de.uka.ilkd.key.speclang.SetOfOperationContract; -import de.uka.ilkd.key.speclang.SpecExtractor; -import de.uka.ilkd.key.speclang.jml.pretranslation.Behavior; -import de.uka.ilkd.key.speclang.jml.pretranslation.SLListOfTextualJMLConstruct; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLClassInv; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLFieldDecl; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec; -import de.uka.ilkd.key.speclang.jml.pretranslation.KeYJMLPreParser; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase; -import de.uka.ilkd.key.speclang.jml.pretranslation.ListOfTextualJMLConstruct; +import de.uka.ilkd.key.speclang.*; +import de.uka.ilkd.key.speclang.jml.pretranslation.*; import de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory; import de.uka.ilkd.key.speclang.translation.SLTranslationException; - +import de.uka.ilkd.key.speclang.translation.SLWarningException; /** - * Extracts JML class invariants and operation contracts from JML comments. - * This is the public interface to the jml package. + * Extracts JML class invariants and operation contracts from JML comments. + * This is the public interface to the jml package. */ public class JMLSpecExtractor implements SpecExtractor { - + private final Services services; private final JMLSpecFactory jsf; + private SetOfPositionedString warnings + = SetAsListOfPositionedString.EMPTY_SET; //------------------------------------------------------------------------- //constructors //------------------------------------------------------------------------- - + public JMLSpecExtractor(Services services) { this.services = services; this.jsf = new JMLSpecFactory(services); } - + //------------------------------------------------------------------------- //internal methods //------------------------------------------------------------------------- - + /** - * Concatenates the passed comments in a position-preserving way. - * (see also JMLTransformer::concatenate(), which does the same thing - * for Recoder ASTs) - */ + * Concatenates the passed comments in a position-preserving way. (see also + * JMLTransformer::concatenate(), which does the same thing for Recoder + * ASTs) + */ private String concatenate(Comment[] comments) { if(comments.length == 0) { return ""; - } + } StringBuffer sb = new StringBuffer(comments[0].getText()); - + for(int i = 1; i < comments.length; i++) { Position relativePos = comments[i].getRelativePosition(); for(int j = 0; j < relativePos.getLine(); j++) { @@ -93,12 +80,12 @@ private String concatenate(Comment[] comments) { } sb.append(comments[i].getText()); } - + return sb.toString(); } + - - private int getIndexOfMethodDecl(ProgramMethod pm, + private int getIndexOfMethodDecl(ProgramMethod pm, TextualJMLConstruct[] constructsArray) { for(int i = 0; i < constructsArray.length; i++) { if(constructsArray[i] instanceof TextualJMLMethodDecl) { @@ -111,96 +98,95 @@ private int getIndexOfMethodDecl(ProgramMethod pm, } return -1; } + - - private void transformFieldDecl(TextualJMLFieldDecl decl, + private void transformFieldDecl(TextualJMLFieldDecl decl, KeYJavaType classKjt) throws SLTranslationException { if(!decl.getMods().contains("model")) { return; } - + String[] splittedDecl = decl.getDecl().text.split(" "); if(splittedDecl.length != 2) { throw new SLTranslationException( - "Unexpected structure of model field declaration!", - decl.getDecl().fileName, - decl.getDecl().pos); + "Unexpected structure of model field declaration!", + decl.getDecl().fileName, + decl.getDecl().pos); } String typeName = splittedDecl[0]; String fieldName = splittedDecl[1].substring(0, splittedDecl[1].length() - 1); - + Sort sort; ArrayOfSort argSorts; try { sort = services.getJavaInfo().getTypeByClassName(typeName).getSort(); - argSorts = decl.getMods().contains("static") + argSorts = decl.getMods().contains("static") ? new ArrayOfSort() : new ArrayOfSort(classKjt.getSort()); } catch(Throwable e) { - throw new SLTranslationException(e.getMessage() - + " (" + throw new SLTranslationException(e.getMessage() + + " (" + e.getClass().getName() - + ")", - decl.getDecl().fileName, - decl.getDecl().pos, + + ")", + decl.getDecl().fileName, + decl.getDecl().pos, e.getStackTrace()); } - - NonRigidHeapDependentFunction f + + NonRigidHeapDependentFunction f = new NonRigidHeapDependentFunction(new Name(fieldName), sort, argSorts); services.getNamespaces().functions().add(f); } - + private String getDefaultSignalsOnly(ProgramMethod pm) { - - if (pm.getThrown() == null) { + if(pm.getThrown() == null) { return "\\nothing;"; } - + ArrayOfTypeReference exceptions = pm.getThrown().getExceptions(); - if (exceptions == null) { + if(exceptions == null) { return "\\nothing;"; } - + String exceptionsString = ""; - for (int i = 0; i < exceptions.size(); i++) { + for(int i = 0; i < exceptions.size(); i++) { //only subtypes of java.lang.Exception are in the default //signals-only - if (services.getJavaInfo().isSubtype( + if(services.getJavaInfo().isSubtype( exceptions.getTypeReference(i).getKeYJavaType(), services.getJavaInfo() .getKeYJavaType("java.lang.Exception"))) { - exceptionsString += exceptions.getTypeReference(i).getName() - + ", "; + exceptionsString + += exceptions.getTypeReference(i).getName() + ", "; } } - if (exceptionsString.equals("")) { + if(exceptionsString.equals("")) { exceptionsString = "\\nothing"; } else { //delete the last ", " - exceptionsString = exceptionsString.substring(0, exceptionsString - .length() - 2); + exceptionsString + = exceptionsString.substring(0, exceptionsString.length() - 2); } return exceptionsString + ";"; } - + //------------------------------------------------------------------------- //public interface //------------------------------------------------------------------------- - - public SetOfClassInvariant extractClassInvariants(KeYJavaType kjt) + + public SetOfClassInvariant extractClassInvariants(KeYJavaType kjt) throws SLTranslationException { SetOfClassInvariant result = SetAsListOfClassInvariant.EMPTY_SET; @@ -208,91 +194,97 @@ public SetOfClassInvariant extractClassInvariants(KeYJavaType kjt) if(!(kjt.getJavaType() instanceof TypeDeclaration)) { return result; } - + //get type declaration, file name TypeDeclaration td = (TypeDeclaration) kjt.getJavaType(); String fileName = td.getPositionInfo().getFileName(); - + //add invariants for non_null fields ArrayOfMemberDeclaration fds = td.getMembers(); - for(int i = 0, m = fds.size(); i < m; i++) { + for(int i = 0, m = fds.size(); i < m; i++) { if(fds.getMemberDeclaration(i) instanceof FieldDeclaration) { - FieldDeclaration fd - = (FieldDeclaration) fds.getMemberDeclaration(i); - ArrayOfFieldSpecification fields = fd.getFieldSpecifications(); - for(int j = 0, n = fields.size(); j < n; j++) { - FieldSpecification field = fields.getFieldSpecification(j); + FieldDeclaration fd + = (FieldDeclaration) fds.getMemberDeclaration(i); + ArrayOfFieldSpecification fields = fd.getFieldSpecifications(); + for(int j = 0, n = fields.size(); j < n; j++) { + FieldSpecification field = fields.getFieldSpecification(j); String fieldName = field.getProgramName(); - // add invariant only for fields of reference types - // and not for implicit fields. + //add invariant only for fields of reference types + //and not for implicit fields. if(services.getTypeConverter().isReferenceType(field.getType()) - && !(field instanceof ImplicitFieldSpecification)) { + && !(field instanceof ImplicitFieldSpecification)) { if(!JMLInfoExtractor.isNullable(fieldName, kjt)) { PositionedString ps = new PositionedString(fieldName + " != null", - fileName, + fileName, fd.getEndPosition()); - result = result.add(jsf.createJMLClassInvariant(kjt, ps)); + result = result.add(jsf.createJMLClassInvariant(kjt, + ps)); } - } - } + } + } } } - - //iterate over all children + + //iterate over all children for(int i = 0, n = td.getChildCount(); i <= n; i++) { - //collect comments + //collect comments //(last position are comments of type declaration itself) Comment[] comments = null; if(i < n) { ProgramElement child = td.getChildAt(i); comments = child.getComments(); - //skip model and ghost elements + //skip model and ghost elements //(their comments are duplicates of other comments) - if((child instanceof FieldDeclaration - && ((FieldDeclaration) child).isGhost()) - || (child instanceof ProgramMethod + if((child instanceof FieldDeclaration + && ((FieldDeclaration) child).isGhost()) + || (child instanceof ProgramMethod && ((ProgramMethod) child).isModel())) { continue; } } else if(td.getComments() != null) { comments = td.getComments(); - } + } if(comments.length == 0) { continue; } - + //concatenate comments, determine position String concatenatedComment = concatenate(comments); Position pos = comments[0].getStartPosition(); - + //call preparser KeYJMLPreParser preParser = new KeYJMLPreParser(concatenatedComment, fileName, pos); ListOfTextualJMLConstruct constructs = preParser.parseClasslevelComment(); - + warnings = warnings.union(preParser.getWarnings()); + //create class invs out of textual constructs, add them to result for(TextualJMLConstruct c : constructs) { if(c instanceof TextualJMLClassInv) { - TextualJMLClassInv textualInv = (TextualJMLClassInv) c; - ClassInvariant inv - = jsf.createJMLClassInvariant(kjt, textualInv); - result = result.add(inv); + try { + TextualJMLClassInv textualInv = (TextualJMLClassInv) c; + ClassInvariant inv + = jsf.createJMLClassInvariant(kjt, textualInv); + result = result.add(inv); + } catch (SLWarningException e) { + warnings = warnings.add(e.getWarning()); + } } else if(c instanceof TextualJMLFieldDecl) { - transformFieldDecl((TextualJMLFieldDecl)c, kjt); + transformFieldDecl((TextualJMLFieldDecl) c, kjt); } - } + } } - return result; + return result; } - - public SetOfOperationContract extractOperationContracts(ProgramMethod pm) + + public SetOfOperationContract extractOperationContracts(ProgramMethod pm) throws SLTranslationException { SetOfOperationContract result = SetAsListOfOperationContract.EMPTY_SET; - + //get type declaration, file name TypeDeclaration td = (TypeDeclaration) pm.getContainerType().getJavaType(); @@ -302,32 +294,34 @@ public SetOfOperationContract extractOperationContracts(ProgramMethod pm) final boolean isPure = JMLInfoExtractor.isPure(pm); if(isPure) { TextualJMLSpecCase sc - = new TextualJMLSpecCase(SLListOfString.EMPTY_LIST, - Behavior.NONE); + = new TextualJMLSpecCase(SLListOfString.EMPTY_LIST, + Behavior.NONE); sc.addAssignable(new PositionedString("\\nothing")); - SetOfOperationContract contracts - = jsf.createJMLOperationContractsAndInherit(pm, sc); + SetOfOperationContract contracts + = jsf.createJMLOperationContractsAndInherit(pm, sc); result = result.union(contracts); } //get textual JML constructs - Comment[] comments = pm.getComments(); + Comment[] comments = pm.getComments(); ListOfTextualJMLConstruct constructs; - if (comments.length != 0) { + if(comments.length != 0) { //concatenate comments, determine position String concatenatedComment = concatenate(comments); Position pos = comments[0].getStartPosition(); + //call preparser KeYJMLPreParser preParser = new KeYJMLPreParser(concatenatedComment, fileName, pos); constructs = preParser.parseClasslevelComment(); + warnings = warnings.union(preParser.getWarnings()); } else { constructs = SLListOfTextualJMLConstruct.EMPTY_LIST; } - + //create JML contracts out of constructs, add them to result TextualJMLConstruct[] constructsArray = constructs.toArray(); - + int startPos; if(pm.isModel()) { startPos = getIndexOfMethodDecl(pm, constructsArray) - 1; @@ -336,105 +330,115 @@ public SetOfOperationContract extractOperationContracts(ProgramMethod pm) startPos = constructsArray.length - 1; } for(int i = startPos; - i >= 0 && constructsArray[i] instanceof TextualJMLSpecCase; + i >= 0 && constructsArray[i] instanceof TextualJMLSpecCase; i--) { TextualJMLSpecCase specCase = (TextualJMLSpecCase) constructsArray[i]; - - if (isPure) { + + if(isPure) { specCase.addDiverges(new PositionedString("false")); - if (!pm.isConstructor()) { + if(!pm.isConstructor()) { specCase.addAssignable(new PositionedString("\\nothing")); } else { specCase.addAssignable(new PositionedString("this.*")); } } - + //add non-null preconditions - for (int j = 0, n = pm.getParameterDeclarationCount(); j < n; j++) { - Type t = pm.getParameterDeclarationAt(j). - getTypeReference(). - getKeYJavaType(); - // no additional precondition for primitive types! - if (services.getTypeConverter().isReferenceType(t) + for(int j = 0, n = pm.getParameterDeclarationCount(); j < n; j++) { + Type t = pm.getParameterDeclarationAt(j).getTypeReference() + .getKeYJavaType(); + //no additional precondition for primitive types! + if(services.getTypeConverter().isReferenceType(t) && !JMLInfoExtractor.parameterIsNullable(pm, j)) { - String param_name = pm. - getParameterDeclarationAt(j). - getVariableSpecification(). - getName(); + String param_name + = pm.getParameterDeclarationAt(j) + .getVariableSpecification().getName(); String nonNull = param_name + " != null"; - specCase.addRequires(new PositionedString( - nonNull, - fileName, - pm.getStartPosition())); + specCase.addRequires( + new PositionedString(nonNull, + fileName, + pm.getStartPosition())); } } - + //add non-null postcondition KeYJavaType resultType = pm.getKeYJavaType(); if(resultType != null - && services.getTypeConverter().isReferenceType(resultType) - && !JMLInfoExtractor.resultIsNullable(pm) - && specCase.getBehavior() != Behavior.EXCEPTIONAL_BEHAVIOR) { + && services.getTypeConverter().isReferenceType(resultType) + && !JMLInfoExtractor.resultIsNullable(pm) + && specCase.getBehavior() != Behavior.EXCEPTIONAL_BEHAVIOR) { String nonNull = "\\result " + " != null"; - specCase.addEnsures(new PositionedString( - nonNull, - fileName, - pm.getStartPosition())); + specCase.addEnsures(new PositionedString(nonNull, fileName, pm + .getStartPosition())); } - - // add implicit signals-only if omitted - if (specCase.getSignalsOnly().isEmpty() - && specCase.getBehavior() != Behavior.NORMAL_BEHAVIOR) { - specCase.addSignalsOnly(new PositionedString( - getDefaultSignalsOnly(pm))); + + //add implicit signals-only if omitted + if(specCase.getSignalsOnly().isEmpty() + && specCase.getBehavior() != Behavior.NORMAL_BEHAVIOR) { + specCase.addSignalsOnly( + new PositionedString(getDefaultSignalsOnly(pm))); + } + + //translate contract + try { + SetOfOperationContract contracts + = jsf.createJMLOperationContractsAndInherit(pm, specCase); + result = result.union(contracts); + } catch (SLWarningException e) { + warnings = warnings.add(e.getWarning()); } - - SetOfOperationContract contracts - = jsf.createJMLOperationContractsAndInherit(pm, specCase); - result = result.union(contracts); } - - return result; + + return result; } + - - public LoopInvariant extractLoopInvariant(ProgramMethod pm, + public LoopInvariant extractLoopInvariant(ProgramMethod pm, LoopStatement loop) throws SLTranslationException { LoopInvariant result = null; - + //get type declaration, file name TypeDeclaration td = (TypeDeclaration) pm.getContainerType().getJavaType(); String fileName = td.getPositionInfo().getFileName(); - + //get comments Comment[] comments = loop.getComments(); if(comments.length == 0) { return result; } - + //concatenate comments, determine position String concatenatedComment = concatenate(comments); Position pos = comments[0].getStartPosition(); - + //call preparser KeYJMLPreParser preParser = new KeYJMLPreParser(concatenatedComment, fileName, pos); ListOfTextualJMLConstruct constructs = preParser.parseMethodlevelComment(); - + warnings = warnings.union(preParser.getWarnings()); + //create JML loop invariant out of last construct if(constructs.size() == 0) { return result; } TextualJMLConstruct c = constructs.take(constructs.size() - 1).head(); if(c instanceof TextualJMLLoopSpec) { - TextualJMLLoopSpec textualLoopSpec = (TextualJMLLoopSpec) c; - result = jsf.createJMLLoopInvariant(pm, loop, textualLoopSpec); + try { + TextualJMLLoopSpec textualLoopSpec = (TextualJMLLoopSpec) c; + result = jsf.createJMLLoopInvariant(pm, loop, textualLoopSpec); + } catch (SLWarningException e) { + warnings = warnings.add(e.getWarning()); + } } - + return result; } + + public SetOfPositionedString getWarnings() { + return JMLTransformer.getWarningsOfLastInstance().union(warnings); + } } diff --git a/system/de/uka/ilkd/key/speclang/jml/pretranslation/jmlpreparser.g b/system/de/uka/ilkd/key/speclang/jml/pretranslation/jmlpreparser.g index 9b0a4336f2c..0a8518babf3 100644 --- a/system/de/uka/ilkd/key/speclang/jml/pretranslation/jmlpreparser.g +++ b/system/de/uka/ilkd/key/speclang/jml/pretranslation/jmlpreparser.g @@ -16,11 +16,8 @@ header { import de.uka.ilkd.key.collection.ListOfString; import de.uka.ilkd.key.collection.SLListOfString; import de.uka.ilkd.key.java.Position; - import de.uka.ilkd.key.speclang.ListOfPositionedString; - import de.uka.ilkd.key.speclang.PositionedString; - import de.uka.ilkd.key.speclang.SLListOfPositionedString; - import de.uka.ilkd.key.speclang.translation.SLTranslationException; - import de.uka.ilkd.key.speclang.translation.SLTranslationExceptionManager; + import de.uka.ilkd.key.speclang.*; + import de.uka.ilkd.key.speclang.translation.*; } @@ -37,6 +34,8 @@ options { { private KeYJMLPreLexer lexer; private SLTranslationExceptionManager excManager; + private SetOfPositionedString warnings + = SetAsListOfPositionedString.EMPTY_SET; private KeYJMLPreParser(KeYJMLPreLexer lexer, @@ -71,9 +70,10 @@ options { private void raiseNotSupported(String feature) - throws SLTranslationException { - throw excManager.createException("JML feature not supported: " - + feature); + throws SLTranslationException { + PositionedString warning + = excManager.createPositionedString(feature + " not supported"); + warnings = warnings.add(warning); } @@ -94,7 +94,12 @@ options { } catch(ANTLRException e) { throw excManager.convertException(e); } - } + } + + + public SetOfPositionedString getWarnings() { + return warnings; + } } @@ -518,7 +523,7 @@ simple_spec_body_clause[TextualJMLSpecCase sc, Behavior b] | ps=signals_clause { sc.addSignals(ps); } | ps=signals_only_clause { sc.addSignalsOnly(ps); } | ps=diverges_clause { sc.addDiverges(ps); } - | ps=name_clause { sc.addName(ps);} + | ps=name_clause { sc.addName(ps);} | captures_clause | when_clause | working_space_clause @@ -649,9 +654,9 @@ name_clause throws SLTranslationException : spec:SPEC_NAME name:STRING_LITERAL SEMICOLON - { - result=createPositionedString(name.getText(), spec); - } + { + result=createPositionedString(name.getText(), spec); + } ; @@ -782,6 +787,7 @@ history_constraint[ListOfString mods] constraint_keyword ps=expression { raiseNotSupported("history constraints"); + result = SLListOfTextualJMLConstruct.EMPTY_LIST; } ; @@ -803,6 +809,7 @@ represents_clause[ListOfString mods] represents_keyword ps=expression { raiseNotSupported("represents clauses"); + result = SLListOfTextualJMLConstruct.EMPTY_LIST; } ; @@ -824,6 +831,7 @@ initially_clause[ListOfString mods] INITIALLY ps=expression { raiseNotSupported("initially clauses"); + result = SLListOfTextualJMLConstruct.EMPTY_LIST; } ; @@ -838,6 +846,7 @@ monitors_for_clause[ListOfString mods] MONITORS_FOR ps=expression { raiseNotSupported("monitors_for clauses"); + result = SLListOfTextualJMLConstruct.EMPTY_LIST; } ; @@ -852,6 +861,7 @@ readable_if_clause[ListOfString mods] READABLE ps=expression { raiseNotSupported("readable-if clauses"); + result = SLListOfTextualJMLConstruct.EMPTY_LIST; } ; @@ -866,6 +876,7 @@ writable_if_clause[ListOfString mods] WRITABLE ps=expression { raiseNotSupported("writable-if clauses"); + result = SLListOfTextualJMLConstruct.EMPTY_LIST; } ; @@ -926,6 +937,7 @@ nowarn_pragma[ListOfString mods] NOWARN ps=expression { raiseNotSupported("nowarn pragmas"); + result = SLListOfTextualJMLConstruct.EMPTY_LIST; } ; @@ -1032,6 +1044,7 @@ assert_statement[ListOfString mods] assert_keyword ps=expression { raiseNotSupported("JML assert statements"); + result = SLListOfTextualJMLConstruct.EMPTY_LIST; } ; @@ -1053,6 +1066,7 @@ assume_statement[ListOfString mods] assume_keyword ps=expression { raiseNotSupported("assume statements"); + result = SLListOfTextualJMLConstruct.EMPTY_LIST; } ; diff --git a/system/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/system/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index dfd2026ff54..8cf4bbacae1 100644 --- a/system/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/system/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -341,8 +341,8 @@ private SetOfOperationContract createJMLOperationContracts( FormulaWithAxioms post = post1.conjoin(post2); if(diverges.equals(FormulaWithAxioms.FF)) { String name = getContractName(originalBehavior); - String customStr = (customName.toString().length() > 0 - ? customName + "[" + name + "]" + String customStr = (customName.text.length() > 0 + ? customName.text + " [" + name + "]" : name); OperationContract contract = new OperationContractImpl(name, diff --git a/system/de/uka/ilkd/key/speclang/jml/translation/jmlparser.g b/system/de/uka/ilkd/key/speclang/jml/translation/jmlparser.g index a7134697acf..10d4f089cf1 100644 --- a/system/de/uka/ilkd/key/speclang/jml/translation/jmlparser.g +++ b/system/de/uka/ilkd/key/speclang/jml/translation/jmlparser.g @@ -17,53 +17,16 @@ header { import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Position; import de.uka.ilkd.key.java.Services; - import de.uka.ilkd.key.java.abstraction.ArrayType; - import de.uka.ilkd.key.java.abstraction.Field; - import de.uka.ilkd.key.java.abstraction.IteratorOfField; - import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType; - import de.uka.ilkd.key.java.abstraction.KeYJavaType; - import de.uka.ilkd.key.java.abstraction.ListOfField; - import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType; - import de.uka.ilkd.key.java.abstraction.PrimitiveType; - import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType; + import de.uka.ilkd.key.java.abstraction.*; import de.uka.ilkd.key.java.declaration.ArrayDeclaration; import de.uka.ilkd.key.java.declaration.ClassDeclaration; import de.uka.ilkd.key.java.expression.literal.BooleanLiteral; import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder; - import de.uka.ilkd.key.logic.BasicLocationDescriptor; - import de.uka.ilkd.key.logic.EverythingLocationDescriptor; - import de.uka.ilkd.key.logic.IteratorOfTerm; - import de.uka.ilkd.key.logic.ListOfTerm; - import de.uka.ilkd.key.logic.LocationDescriptor; - import de.uka.ilkd.key.logic.Name; - import de.uka.ilkd.key.logic.SetAsListOfLocationDescriptor; - import de.uka.ilkd.key.logic.SetOfLocationDescriptor; - import de.uka.ilkd.key.logic.SLListOfTerm; - import de.uka.ilkd.key.logic.Term; - import de.uka.ilkd.key.logic.TermBuilder; - import de.uka.ilkd.key.logic.TermCreationException; + import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.ldt.LDT; import de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT; - import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable; - import de.uka.ilkd.key.logic.op.ExactInstanceSymbol; - import de.uka.ilkd.key.logic.op.Function; - import de.uka.ilkd.key.logic.op.InstanceofSymbol; - import de.uka.ilkd.key.logic.op.IteratorOfLogicVariable; - import de.uka.ilkd.key.logic.op.IteratorOfParsableVariable; - import de.uka.ilkd.key.logic.op.ListOfLogicVariable; - import de.uka.ilkd.key.logic.op.ListOfParsableVariable; - import de.uka.ilkd.key.logic.op.LogicVariable; - import de.uka.ilkd.key.logic.op.NonRigid; - import de.uka.ilkd.key.logic.op.Operator; - import de.uka.ilkd.key.logic.op.ParsableVariable; - import de.uka.ilkd.key.logic.op.ProgramVariable; - import de.uka.ilkd.key.logic.op.RigidFunction; - import de.uka.ilkd.key.logic.op.SLListOfLogicVariable; - import de.uka.ilkd.key.logic.sort.AbstractSort; - import de.uka.ilkd.key.logic.sort.ArraySort; - import de.uka.ilkd.key.logic.sort.ObjectSort; - import de.uka.ilkd.key.logic.sort.Sort; - import de.uka.ilkd.key.logic.sort.SortDefiningSymbols; + import de.uka.ilkd.key.logic.op.*; + import de.uka.ilkd.key.logic.sort.*; import de.uka.ilkd.key.proof.AtPreFactory; import de.uka.ilkd.key.proof.OpReplacer; import de.uka.ilkd.key.proof.init.CreatedAttributeTermFactory; @@ -203,8 +166,7 @@ options { private void raiseNotSupported(String feature) throws SLTranslationException { - throw excManager.createException("JML feature not supported: " - + feature); + throw excManager.createWarningException(feature + " not supported"); } diff --git a/system/de/uka/ilkd/key/speclang/ocl/OCLSpecExtractor.java b/system/de/uka/ilkd/key/speclang/ocl/OCLSpecExtractor.java index 3c6da32ab4a..ecd69fd9b44 100644 --- a/system/de/uka/ilkd/key/speclang/ocl/OCLSpecExtractor.java +++ b/system/de/uka/ilkd/key/speclang/ocl/OCLSpecExtractor.java @@ -16,13 +16,7 @@ import de.uka.ilkd.key.java.declaration.TypeDeclaration; import de.uka.ilkd.key.java.statement.LoopStatement; import de.uka.ilkd.key.logic.op.ProgramMethod; -import de.uka.ilkd.key.speclang.ClassInvariant; -import de.uka.ilkd.key.speclang.LoopInvariant; -import de.uka.ilkd.key.speclang.SetAsListOfClassInvariant; -import de.uka.ilkd.key.speclang.SetAsListOfOperationContract; -import de.uka.ilkd.key.speclang.SetOfClassInvariant; -import de.uka.ilkd.key.speclang.SetOfOperationContract; -import de.uka.ilkd.key.speclang.SpecExtractor; +import de.uka.ilkd.key.speclang.*; import de.uka.ilkd.key.speclang.ocl.translation.OCLSpecFactory; import de.uka.ilkd.key.speclang.translation.SLTranslationException; @@ -162,4 +156,11 @@ public LoopInvariant extractLoopInvariant(ProgramMethod pm, LoopStatement loop) throws SLTranslationException { return null; //OCL has no loop invariants } + + + + public SetOfPositionedString getWarnings() { + //graceful treatment of unsupported features for OCL not implemented + return SetAsListOfPositionedString.EMPTY_SET; + } } diff --git a/system/de/uka/ilkd/key/speclang/translation/SLTranslationExceptionManager.java b/system/de/uka/ilkd/key/speclang/translation/SLTranslationExceptionManager.java index 8fe02b4719d..83cfdc69523 100644 --- a/system/de/uka/ilkd/key/speclang/translation/SLTranslationExceptionManager.java +++ b/system/de/uka/ilkd/key/speclang/translation/SLTranslationExceptionManager.java @@ -88,6 +88,16 @@ public PositionedString createPositionedString(String text, Token t) { } + /** + * Creates a string with the current absolute position information + */ + public PositionedString createPositionedString(String text) { + return new PositionedString(text, + fileName, + getPosition()); + } + + /** * Creates an SLTranslationException with current absolute position * information. @@ -97,7 +107,7 @@ public SLTranslationException createException(String message) { fileName, getPosition()); } - + /** * Creates an SLTranslationException with the position information of the @@ -109,6 +119,17 @@ public SLTranslationException createException(String message, Token t) { createAbsolutePosition(t.getLine(), t.getColumn())); } + + + /** + * Creates an SLWarningException with current absolute position + * information. + */ + public SLTranslationException createWarningException(String message) { + return new SLWarningException(message, + fileName, + getPosition()); + } /** diff --git a/system/de/uka/ilkd/key/speclang/translation/SLWarningException.java b/system/de/uka/ilkd/key/speclang/translation/SLWarningException.java new file mode 100644 index 00000000000..973eabb7de6 --- /dev/null +++ b/system/de/uka/ilkd/key/speclang/translation/SLWarningException.java @@ -0,0 +1,32 @@ +// This file is part of KeY - Integrated Deductive Software Design +// Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany +// Universitaet Koblenz-Landau, Germany +// Chalmers University of Technology, Sweden +// +// The KeY system is protected by the GNU General Public License. +// See LICENSE.TXT for details. +// +// + +package de.uka.ilkd.key.speclang.translation; + +import de.uka.ilkd.key.java.Position; +import de.uka.ilkd.key.speclang.PositionedString; + + +public class SLWarningException extends SLTranslationException { + + public SLWarningException(String text, String fileName, Position pos) { + super(text, fileName, pos); + } + + + public SLWarningException(PositionedString warning) { + this(warning.text, warning.fileName, warning.pos); + } + + + public PositionedString getWarning() { + return new PositionedString(getMessage(), getFileName(), getPosition()); + } +}