Skip to content

Commit 41fe34a

Browse files
wadoonwadoon
committed
assumption
1 parent ed131ae commit 41fe34a

File tree

5 files changed

+65
-37
lines changed

5 files changed

+65
-37
lines changed

‎key.core/src/main/antlr4/JmlLexer.g4‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -485,6 +485,7 @@ CHAR_LITERAL:
485485
fragment OCT_CHAR:
486486
(('0'|'1'|'2'|'3') OCTDIGIT OCTDIGIT) | (OCTDIGIT OCTDIGIT) | OCTDIGIT;
487487

488+
KEY_TERM : '`' ~([`])* '`';
488489
STRING_LITERAL: '"' -> pushMode(string),more;
489490
E_WS: [ \t\n\r\u000c@]+ -> channel(HIDDEN), type(WS);
490491
INFORMAL_DESCRIPTION: '(*' ( '*' ~')' | ~'*' )* '*)';

‎key.core/src/main/antlr4/JmlParser.g4‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -376,6 +376,7 @@ jmlprimary
376376
| SUBSET LPAREN storeref COMMA storeref RPAREN #primarySubset
377377
| NEWELEMSFRESH LPAREN storeref RPAREN #primaryNewElemsfrehs
378378
| sequence #primaryignore10
379+
| KEY_TERM #keyTerm
379380
;
380381

381382
sequence
@@ -408,5 +409,4 @@ type: builtintype | referencetype | TYPE;
408409
referencetype: name;
409410
builtintype: BYTE | SHORT | INT | LONG | BOOLEAN | VOID | BIGINT | REAL | LOCSET | SEQ | FREE;
410411
name: ident (DOT ident)*;
411-
quantifiedvariabledeclarator: IDENT dims?;
412-
412+
quantifiedvariabledeclarator: IDENT dims?;

‎key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/RecordClassBuilder.java‎

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,12 @@
1414
import com.github.javaparser.ast.body.*;
1515
import com.github.javaparser.ast.expr.*;
1616
import com.github.javaparser.ast.key.JmlDocModifier;
17+
import com.github.javaparser.ast.key.KeYMarkerStatement;
1718
import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName;
1819
import com.github.javaparser.ast.stmt.ReturnStmt;
1920
import com.github.javaparser.ast.type.PrimitiveType;
2021
import com.github.javaparser.ast.type.Type;
22+
import de.uka.ilkd.key.java.transformations.MarkerStatementHelper;
2123
import org.jspecify.annotations.Nullable;
2224

2325
import static com.github.javaparser.ast.Modifier.DefaultKeyword.*;
@@ -134,24 +136,24 @@ private void createConstructor(RecordDeclaration recordDeclaration,
134136
body.addStatement(
135137
assign(attributeThis(p.getNameAsString()), p.getNameAsExpression()));
136138
}
137-
138-
var fieldParamEqual = recordDeclaration.getParameters()
139-
.stream()
140-
.map(NodeWithSimpleName::getNameAsString)
141-
.map(it -> "ensures this.%s == %s;".formatted(it, it))
142-
.collect(Collectors.joining("\n"));
143-
services.attachSpec(fullConstructor, """
144-
public normal_behavior
145-
requires true;
146-
%s
147-
""".formatted(fieldParamEqual));
148-
149139
}
150140

151141
for (var compactConstructor : recordDeclaration.getCompactConstructors()) {
152142
fullConstructor.getBody().get().getStatements().add(0, compactConstructor.getBody());
153143
}
154144

145+
var type = recordDeclaration.getNameAsString();
146+
var marker = new KeYMarkerStatement(MarkerStatementHelper.KIND_ASSUME);
147+
var fieldParamEqual = recordDeclaration.getParameters()
148+
.stream()
149+
.map(NodeWithSimpleName::getNameAsString)
150+
.map(it -> "(`int::select(heap, self, %s::#%s)` == this.%s)".formatted(type, it, it))
151+
.collect(Collectors.joining(" && "));
152+
153+
services.attachExpr(marker,
154+
"//@ assume %s;".formatted(fieldParamEqual));
155+
fullConstructor.getBody().get().addStatement(marker);
156+
155157
clazz.addMember(fullConstructor);
156158
}
157159

@@ -214,7 +216,7 @@ private boolean createEquals(RecordDeclaration recordDeclaration,
214216
equals.addAnnotation(Override.class);
215217
equals.setType(Boolean.TYPE);
216218
Type tObject = StaticJavaParser.parseType("java.lang.Object");
217-
var mods = new NodeList<>(new Modifier(JML_NULLABLE));
219+
var mods = new NodeList<Modifier>(/*new Modifier(JML_NULLABLE)*/);
218220
equals.getParameters().add(new Parameter(mods, tObject, new SimpleName("o")));
219221
equals.setBody(null);
220222

‎key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java‎

Lines changed: 32 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -3,19 +3,6 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.java.transformations.pipeline;
55

6-
import java.util.*;
7-
import java.util.stream.Collectors;
8-
9-
import de.uka.ilkd.key.java.loader.JavaParserFactory;
10-
import de.uka.ilkd.key.java.transformations.ConstantExpressionEvaluator;
11-
import de.uka.ilkd.key.java.transformations.EvaluationException;
12-
import de.uka.ilkd.key.speclang.PositionedString;
13-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
14-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
15-
import de.uka.ilkd.key.speclang.njml.PreParser;
16-
17-
import org.key_project.util.collection.ImmutableList;
18-
196
import com.github.javaparser.JavaParser;
207
import com.github.javaparser.ast.CompilationUnit;
218
import com.github.javaparser.ast.Modifier;
@@ -31,20 +18,35 @@
3118
import com.github.javaparser.resolution.model.SymbolReference;
3219
import com.github.javaparser.resolution.types.ResolvedReferenceType;
3320
import com.github.javaparser.resolution.types.ResolvedType;
21+
import de.uka.ilkd.key.java.Position;
22+
import de.uka.ilkd.key.java.loader.JavaParserFactory;
23+
import de.uka.ilkd.key.java.transformations.ConstantExpressionEvaluator;
24+
import de.uka.ilkd.key.java.transformations.EvaluationException;
25+
import de.uka.ilkd.key.speclang.PositionedString;
26+
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement;
27+
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
28+
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
29+
import de.uka.ilkd.key.speclang.njml.PreParser;
3430
import org.jspecify.annotations.NonNull;
3531
import org.jspecify.annotations.NullMarked;
3632
import org.jspecify.annotations.Nullable;
33+
import org.key_project.util.collection.ImmutableList;
3734
import org.slf4j.Logger;
3835
import org.slf4j.LoggerFactory;
3936

37+
import java.util.*;
38+
import java.util.stream.Collectors;
39+
40+
import static de.uka.ilkd.key.java.transformations.MarkerStatementHelper.KEY_EXPR;
41+
4042
/**
4143
* @author Alexander Weigl
4244
* @version 1 (11/2/21)
4345
*/
4446
@NullMarked
4547
public class TransformationPipelineServices {
4648
private static final Logger LOGGER =
47-
LoggerFactory.getLogger(TransformationPipelineServices.class);
49+
LoggerFactory.getLogger(TransformationPipelineServices.class);
4850

4951
private final TransformerCache cache;
5052

@@ -53,7 +55,7 @@ public class TransformationPipelineServices {
5355
private List<PositionedString> warnings = new ArrayList<>(8);
5456

5557
public TransformationPipelineServices(JavaParserFactory javaParserFactory,
56-
TransformerCache cache) {
58+
TransformerCache cache) {
5759
this.cache = cache;
5860
this.javaParserFactory = javaParserFactory;
5961
}
@@ -139,7 +141,7 @@ public String getId(TypeDeclaration<?> td) {
139141
* according to JLS Sect. 4.5.5
140142
*
141143
* @return the default value of the given type
142-
* according to JLS Sect. 4.5.5
144+
* according to JLS Sect. 4.5.5
143145
*/
144146
public Expression getDefaultValue(Type type) {
145147
if (type instanceof ReferenceType) {
@@ -270,7 +272,7 @@ public NodeList<Statement> getInitializers(ClassOrInterfaceDeclaration cd) {
270272
if (member instanceof InitializerDeclaration init &&
271273
!init.isStatic()) {
272274
String name =
273-
PipelineConstants.OBJECT_INITIALIZER_IDENTIFIER + objectInitializerCount;
275+
PipelineConstants.OBJECT_INITIALIZER_IDENTIFIER + objectInitializerCount;
274276
var initializerMethod = cd.addMethod(name, Modifier.DefaultKeyword.PRIVATE);
275277
initializerMethod.setBody(init.getBody().clone());
276278
initializerMethod.setParentNode(cd);
@@ -282,9 +284,9 @@ public NodeList<Statement> getInitializers(ClassOrInterfaceDeclaration cd) {
282284
if (variable.getInitializer().isPresent()) {
283285
Expression fieldInit = variable.getInitializer().get();
284286
final var access = new FieldAccessExpr(
285-
new ThisExpr(), new NodeList<>(), variable.getName());
287+
new ThisExpr(), new NodeList<>(), variable.getName());
286288
var fieldCopy =
287-
new AssignExpr(access, fieldInit.clone(), AssignExpr.Operator.ASSIGN);
289+
new AssignExpr(access, fieldInit.clone(), AssignExpr.Operator.ASSIGN);
288290
result.add(new ExpressionStmt(fieldCopy));
289291
}
290292
}
@@ -317,8 +319,7 @@ public Expression getDefaultValue(ResolvedType type) {
317319
case "int", "byte", "short" -> new IntegerLiteralExpr("0");
318320
case "char" -> new CharLiteralExpr("0");
319321
case "float", "double" -> new DoubleLiteralExpr("0.0");
320-
default ->
321-
throw new IllegalStateException("Unexpected value: " + name.toLowerCase());
322+
default -> throw new IllegalStateException("Unexpected value: " + name.toLowerCase());
322323
};
323324
}
324325

@@ -360,6 +361,16 @@ public void attachSpec(Node node, @Nullable String spec) {
360361
LOGGER.info("Generated specification {} for {}", spec, node);
361362
}
362363

364+
public void attachExpr(Node node, @Nullable String spec) {
365+
if (spec == null)
366+
return;
367+
PreParser pp = getPreParser();
368+
ImmutableList<TextualJMLConstruct> specification = pp.parseMethodLevel(spec, null, Position.UNDEFINED);
369+
TextualJMLAssertStatement expr = (TextualJMLAssertStatement) specification.get(0);
370+
node.setData(KEY_EXPR, expr.getContext());
371+
LOGGER.info("Generated specification {} for {}", spec, node);
372+
}
373+
363374

364375
/**
365376
* Cache of important data. This is done mainly for performance reasons.

‎key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java‎

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@
2020
import de.uka.ilkd.key.logic.*;
2121
import de.uka.ilkd.key.logic.op.*;
2222
import de.uka.ilkd.key.logic.sort.ArraySort;
23+
import de.uka.ilkd.key.nparser.KeyIO;
2324
import de.uka.ilkd.key.proof.OpReplacer;
2425
import de.uka.ilkd.key.speclang.ClassAxiom;
2526
import de.uka.ilkd.key.speclang.Contract;
@@ -247,7 +248,6 @@ private String createSignatureString(ImmutableList<SLExpression> signature) {
247248
}
248249

249250
// region expression
250-
251251
@Override
252252
public KeYJavaType visitBuiltintype(JmlParser.BuiltintypeContext ctx) {
253253
if (ctx.BYTE() != null) {
@@ -755,6 +755,20 @@ public Object visitAdditiveexpr(JmlParser.AdditiveexprContext ctx) {
755755
return result;
756756
}
757757

758+
759+
@Override
760+
public SLExpression visitKeyTerm(JmlParser.KeyTermContext ctx) {
761+
var key = ctx.KEY_TERM().getText();
762+
key = key.substring(1, key.length() - 1);
763+
var nss = services.getNamespaces().copyWithParent();
764+
nss.programVariables().add(selfVar);
765+
nss.programVariables().add(excVar);
766+
var keyIO = new KeyIO(services, nss);
767+
768+
var term = keyIO.parseExpression(key);
769+
return new SLExpression(term);
770+
}
771+
758772
@Override
759773
public Object visitMultexpr(JmlParser.MultexprContext ctx) {
760774
List<SLExpression> exprs = mapOf(ctx.unaryexpr());

0 commit comments

Comments
 (0)