Skip to content

Commit 0a0979d

Browse files
kruegerskruegers
authored
Merge pull request #335 from AndreSonntag/ensuresPredicatePreAnalyse
Ensures predicate
2 parents 69ad7ab + cd1f36d commit 0a0979d

14 files changed

Lines changed: 1246 additions & 894 deletions

File tree

‎plugins/de.cognicrypt.core/src/de/cognicrypt/core/Constants.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -477,7 +477,7 @@ public String toString() {
477477
public static final String PREDICATEENSURER_GROUPID = "de.upb.cognicrypt.predicateensurer";
478478
public static final String PREDICATEENSURER_ARTIFACTID = "PredicateEnsurer";
479479
public static final String PREDICATEENSURER_VERSION = "0.0.1-SNAPSHOT";
480-
public static final String PREDICATEENSURER_JAR_IMPORT = "de.upb.cognicrypt.predicateensurer.CC";
480+
public static final String PREDICATEENSURER_JAR_IMPORT = "de.upb.cognicrypt.predicateensurer.Ensurer";
481481

482482
public static final String DEPENDENCIES_TAG = "dependencies";
483483
public static final String DEPENDENCY_TAG = "dependency";

‎plugins/de.cognicrypt.core/src/de/cognicrypt/utils/Utils.java‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,8 @@
11
/********************************************************************************
22
* Copyright (c) 2015-2019 TU Darmstadt, Paderborn University
33
*
4-
54
* http://www.eclipse.org/legal/epl-2.0. SPDX-License-Identifier: EPL-2.0
65
********************************************************************************/
7-
86
package de.cognicrypt.utils;
97

108
import java.io.File;
@@ -418,4 +416,13 @@ public static boolean isIncompatibleJavaVersion() {
418416
public static boolean isIncompatibleJavaVersion(String javaVersion) {
419417
return javaVersion == null || !javaVersion.startsWith("1.");
420418
}
419+
420+
/**
421+
* This method checks if a Collection is null or empty
422+
* @param c
423+
* @return
424+
*/
425+
public static boolean isNullOrEmpty( final Collection< ? > c ) {
426+
return c == null || c.isEmpty();
427+
}
421428
}

‎plugins/de.cognicrypt.crysl.handler/META-INF/MANIFEST.MF‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,5 +22,6 @@ Bundle-RequiredExecutionEnvironment: JavaSE-1.8
2222
Bundle-ActivationPolicy: lazy
2323
Bundle-ClassPath: .
2424
Automatic-Module-Name: de.cognicrypt.crysl.handler
25-
Export-Package: de.cognicrypt.crysl.reader
25+
Export-Package: de.cognicrypt.crysl.creator,
26+
de.cognicrypt.crysl.reader
2627
Import-Package: org.junit

‎plugins/de.cognicrypt.crysl.handler/src/main/java/de/cognicrypt/crysl/creator/CrySLRuleCreator.java‎

Lines changed: 222 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,222 @@
1+
package de.cognicrypt.crysl.creator;
2+
3+
import java.io.File;
4+
import java.io.FileOutputStream;
5+
import java.io.IOException;
6+
import java.nio.file.Files;
7+
import java.nio.file.Paths;
8+
import java.util.List;
9+
import com.google.common.base.Strings;
10+
import de.cognicrypt.core.Constants;
11+
import de.cognicrypt.crysl.handler.Activator;
12+
import de.cognicrypt.utils.Utils;
13+
14+
/**
15+
* This class creates programmatically a CrySL rule
16+
* @author André Sonntag
17+
*
18+
*/
19+
public class CrySLRuleCreator {
20+
21+
public CrySLRuleCreator() {}
22+
23+
/**
24+
* This method creates a CrySL rule and compiled them
25+
* @param filePath - path where the file should be stored
26+
* @param spec - fully-qualified name of the class
27+
* @param objects - {@link List<String>} of objects in format: fully-qualified className varName; (i.e."java.lang.Object obj;")
28+
* @param events - {@link List<String>} of events that contribute to successful usage of the class
29+
* @param order - {@link String} regular expression of method event patterns that are defined in @param events
30+
* @param constraints - {@link List<String>} of constraints for objects defined in @param objects
31+
* @param requires - {@link List<String>} of required predicates
32+
* @param ensures - {@link List<String>} of ensured predicates
33+
* @return <CODE>true</CODE>/<CODE>false</CODE> if no error occurs during generation and compiling process
34+
*/
35+
public boolean createRule(String filePath, String spec, List<String> objects, List<String> events, String order,
36+
List<String> constraints, List<String> requires, List<String> ensures) {
37+
38+
if (Strings.isNullOrEmpty(spec) || Utils.isNullOrEmpty(objects) || Utils.isNullOrEmpty(events)
39+
|| Strings.isNullOrEmpty(order) || Utils.isNullOrEmpty(ensures)) {
40+
Activator.getDefault().logError(null, "One or more mandatory sections are null or empty");
41+
return false;
42+
}
43+
44+
final String SPEC = "SPEC " + spec;
45+
final String OBJECTS = buildCrySLSectionString("OBJECTS", objects);
46+
final String EVENTS = buildCrySLSectionString("EVENTS", events);
47+
final String ORDER = "ORDER" + "\n" + "\t" + order;
48+
final String CONSTRAINTS = buildCrySLSectionString("CONSTRAINTS", constraints);
49+
final String REQUIRES = buildCrySLSectionString("REQUIRES", requires);
50+
final String ENSURES = buildCrySLSectionString("ENSURES", ensures);
51+
final String cryslRuleContent = buildCrySLContentString(SPEC, OBJECTS, EVENTS, ORDER, CONSTRAINTS, REQUIRES, ENSURES);
52+
53+
try {
54+
createCrySLFile(filePath, cryslRuleContent);
55+
} catch (IOException e) {
56+
Activator.getDefault().logError(null, Constants.ERROR_MESSAGE_NO_FILE);
57+
}
58+
59+
return true;
60+
}
61+
62+
/**
63+
* This method extends a certain section by further a {@link String}
64+
* @param filePath - Path where the file is stored
65+
* @param section - Section to be extended
66+
* @param content - {@link String} object to extend the section
67+
* @return <CODE>true</CODE>/<CODE>false</CODE> if file and section could be find and no error occurs during compiling process
68+
*/
69+
public boolean extendRule(String filePath, String section, String content) {
70+
File f = new File(filePath);
71+
boolean successful = false;
72+
73+
if (f.exists()) {
74+
try {
75+
List<String> rule = Files.readAllLines(Paths.get(filePath));
76+
for (int i = 0; i < rule.size(); i++) {
77+
if (rule.get(i).trim().toUpperCase().equals(section.trim())) {
78+
boolean doublicate = false;
79+
for(int j = i; j < rule.size(); j++) {
80+
if(rule.get(j).trim().equals(content.trim())) {
81+
doublicate = true;
82+
break;
83+
}
84+
}
85+
if(!doublicate) {
86+
rule.add(i + 1, "\t" + content);
87+
successful = true;
88+
break;
89+
}
90+
}
91+
}
92+
createCrySLFile(f.getAbsolutePath(), rule);
93+
} catch (IOException e) {
94+
Activator.getDefault().logError(null, Constants.ERROR_MESSAGE_NO_FILE);
95+
}
96+
} else {
97+
Activator.getDefault().logError(null, Constants.ERROR_MESSAGE_NO_FILE);
98+
}
99+
return successful;
100+
}
101+
102+
/**
103+
* This method deletes the matched {@link String} from the rule content
104+
* @param filePath Path where the file is stored
105+
* @param {@link String} to be deleted from the rule
106+
* @return <CODE>true</CODE>/<CODE>false</CODE> if file and content sting could be find and no error occurs during compiling process
107+
*/
108+
public boolean reduceRule(String filePath, String content) {
109+
110+
File f = new File(filePath);
111+
boolean successful = false;
112+
113+
if (f.exists()) {
114+
try {
115+
List<String> rule = Files.readAllLines(Paths.get(filePath));
116+
for (int i = 0; i < rule.size(); i++) {
117+
if (rule.get(i).trim().equals(content.trim())) {
118+
rule.remove(i);
119+
successful = true;
120+
break;
121+
}
122+
}
123+
createCrySLFile(f.getAbsolutePath(), rule);
124+
} catch (IOException e) {
125+
Activator.getDefault().logError(null, Constants.ERROR_MESSAGE_NO_FILE);
126+
}
127+
} else {
128+
Activator.getDefault().logError(null, Constants.ERROR_MESSAGE_NO_FILE);
129+
}
130+
return successful;
131+
}
132+
133+
/**
134+
* This method composes the individual sections to a rule
135+
* @param spec - spec {@link String}
136+
* @param objects - objects {@link List<String>}
137+
* @param events - events {@link List<String>}
138+
* @param order - order {@link String}
139+
* @param constraints - constraints {@link List<String>}
140+
* @param requires - requires {@link List<String>}
141+
* @param ensures - ensures {@link List<String>}
142+
* @return composed rule as String
143+
*/
144+
private String buildCrySLContentString(String spec, String objects, String events, String order, String constraints,
145+
String requires, String ensures) {
146+
147+
StringBuilder builder = new StringBuilder();
148+
149+
builder.append(spec);
150+
builder.append("\n");
151+
builder.append(objects);
152+
builder.append("\n");
153+
builder.append(events);
154+
builder.append("\n");
155+
builder.append(order);
156+
builder.append("\n");
157+
builder.append(constraints);
158+
builder.append("\n");
159+
builder.append(requires);
160+
builder.append("\n");
161+
builder.append(ensures);
162+
163+
return builder.toString();
164+
}
165+
166+
/**
167+
* This method checks the format of the values for a certain section, furthermore
168+
* the rule composes the section together
169+
* @param section - {@link String} section name
170+
* @param values - {@link List<String>} with the values for the section
171+
* @return composed section as String
172+
*/
173+
private String buildCrySLSectionString(String section, List<String> values) {
174+
175+
if (Utils.isNullOrEmpty(values)) {
176+
return "";
177+
}
178+
179+
StringBuilder builder = new StringBuilder();
180+
builder.append(section);
181+
builder.append("\n");
182+
183+
for (String value : values) {
184+
String temp = !value.endsWith(";") ? value + ";" : value;
185+
builder.append("\t");
186+
builder.append(temp);
187+
builder.append("\n");
188+
}
189+
return builder.toString();
190+
}
191+
192+
/**
193+
* This method writes the rule content to a file
194+
* @param filePath path where the rule should be stored
195+
* @param content rule content as {@link String}
196+
* @throws IOException
197+
*/
198+
private void createCrySLFile(String filePath, String content) throws IOException {
199+
String path = filePath.endsWith(Constants.cryslFileEnding) ? filePath : filePath + Constants.cryslFileEnding;
200+
FileOutputStream fos = new FileOutputStream(path);
201+
fos.write(content.getBytes());
202+
fos.flush();
203+
fos.close();
204+
}
205+
206+
/**
207+
* This method writes the rule content from {@link List<String>} to a file
208+
* @param filePath path where the rule should be store
209+
* @param content rule content as {@link List<String>}
210+
* @throws IOException
211+
*/
212+
private void createCrySLFile(String filePath, List<String> content) throws IOException {
213+
StringBuilder builder = new StringBuilder();
214+
for (String s : content) {
215+
builder.append(s);
216+
builder.append("\n");
217+
}
218+
createCrySLFile(filePath, builder.toString());
219+
}
220+
221+
222+
}

0 commit comments

Comments
 (0)