Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion sherrloc
Submodule sherrloc updated 39 files
+1 −0 .gitignore
+2 −1 GenErrorDiagnostic/build.xml
+ − GenErrorDiagnostic/lib/SHErrLoc.jar
+91 −43 GenErrorDiagnostic/src/sherrloc/constraint/analysis/CFLPathFinder.java
+48 −37 GenErrorDiagnostic/src/sherrloc/constraint/analysis/ConstraintAnalysisImpl.java
+12 −0 GenErrorDiagnostic/src/sherrloc/constraint/analysis/Evidence.java
+9 −0 GenErrorDiagnostic/src/sherrloc/constraint/analysis/PathFinder.java
+298 −213 GenErrorDiagnostic/src/sherrloc/constraint/analysis/ShortestPathFinder.java
+9 −2 GenErrorDiagnostic/src/sherrloc/constraint/ast/Constraint.java
+35 −16 GenErrorDiagnostic/src/sherrloc/constraint/ast/Hypothesis.java
+54 −39 GenErrorDiagnostic/src/sherrloc/graph/ConstraintGraph.java
+41 −21 GenErrorDiagnostic/src/sherrloc/graph/Graph.java
+74 −0 GenErrorDiagnostic/src/sherrloc/graph/HypothesisSet.java
+3 −3 GenErrorDiagnostic/src/sherrloc/graph/LeftEdge.java
+3 −3 GenErrorDiagnostic/src/sherrloc/graph/LeqEdge.java
+10 −1 GenErrorDiagnostic/src/sherrloc/graph/ReductionEdge.java
+3 −3 GenErrorDiagnostic/src/sherrloc/graph/RightEdge.java
+56 −17 GenErrorDiagnostic/src/sherrloc/test/TestAll.java
+28 −0 GenErrorDiagnostic/src/sherrloc/test/TestHypothesisCache.java
+65 −0 GenErrorDiagnostic/src/sherrloc/test/TestHypothesisPaths.java
+11 −0 GenErrorDiagnostic/tests/hypothesis-cache/first.con
+11 −0 GenErrorDiagnostic/tests/hypothesis-cache/second.con
+10 −0 GenErrorDiagnostic/tests/hypothesis-paths/chain-combined.con
+10 −0 GenErrorDiagnostic/tests/hypothesis-paths/chain-partial_W.con
+10 −0 GenErrorDiagnostic/tests/hypothesis-paths/constructor-entailed.con
+12 −0 GenErrorDiagnostic/tests/hypothesis-paths/constructor-parallel_W.con
+11 −0 GenErrorDiagnostic/tests/hypothesis-paths/cycle-hypothesized.con
+12 −0 GenErrorDiagnostic/tests/hypothesis-paths/cycle-unhypothesized-exit_W.con
+10 −0 GenErrorDiagnostic/tests/hypothesis-paths/join-entailed.con
+12 −0 GenErrorDiagnostic/tests/hypothesis-paths/join-parallel_W.con
+10 −0 GenErrorDiagnostic/tests/hypothesis-paths/join-partial_W.con
+10 −0 GenErrorDiagnostic/tests/hypothesis-paths/parallel-both-entailed.con
+9 −0 GenErrorDiagnostic/tests/hypothesis-paths/parallel-hyp-first_W.con
+9 −0 GenErrorDiagnostic/tests/hypothesis-paths/parallel-hyp-last_W.con
+10 −0 GenErrorDiagnostic/tests/hypothesis-paths/parallel-incomparable_W.con
+12 −0 GenErrorDiagnostic/tests/hypothesis-paths/paths-both-hypothesized.con
+13 −0 GenErrorDiagnostic/tests/hypothesis-paths/paths-incomparable_W.con
+12 −0 GenErrorDiagnostic/tests/hypothesis-paths/paths-one-hypothesized-reordered_W.con
+12 −0 GenErrorDiagnostic/tests/hypothesis-paths/paths-one-hypothesized_W.con
11 changes: 2 additions & 9 deletions src/Preprocessor.java
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,7 @@ public static List<SourceFile> preprocess(List<File> inputFiles) throws IOExcept
for (File builtinFile : Utils.BUILTIN_FILES) {
Symbol result;
try {
result = Parser.parse(builtinFile, null); //p.parse()
assert result != null;
result = Parser.parse(builtinFile, null);
} catch (SyntaxError se) {
continue;
}
Expand Down Expand Up @@ -63,13 +62,7 @@ public static List<SourceFile> preprocess(List<File> inputFiles) throws IOExcept
// add all contracts from inputFiles recursively
while (!mentionedFiles.isEmpty()) {
File file = mentionedFiles.poll();
Symbol result;
try {
result = Parser.parse(file, null); //p.parse()
assert result != null;
} catch (SyntaxError se) {
throw se;
}
Symbol result = Parser.parse(file, null);

List<SourceFile> rootsFiles = (List<SourceFile>) result.value;
if (rootsFiles == null || rootsFiles.isEmpty()) {
Expand Down
145 changes: 73 additions & 72 deletions src/SCIF.cup
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,15 @@ parser code {:
errorMessages.add(sb.toString());
}

/**
* Records an error that is not a syntax error at the given position in the file being
* parsed, which makes {@link #parse()} fail.
*/
void reportError(int left, int right, String message) {
hasError = true;
errorMessages.add(ErrorFormatter.format(filename, left, right, message));
}

@Override public void report_error(String message, Object info) {
// only used by CUP internals; actual reporting is done in syntax_error
hasError = true;
Expand Down Expand Up @@ -99,35 +108,39 @@ parser code {:
parse(inputFile, null);
} catch (SyntaxError err) {
/* ignore */
} catch (FileNotFoundException e) {
System.err.println("File not found: " + e.getMessage());
}
}

public static Symbol parse(File inputFile, File astFile) throws SyntaxError {
Symbol rtn = null;
/**
* Parses {@code inputFile}, writing the AST to {@code astFile} if it is not null.
*
* @throws SyntaxError if the file has syntax errors or imports a file that does not exist
* @throws FileNotFoundException if {@code inputFile} cannot be read
*/
public static Symbol parse(File inputFile, File astFile)
throws SyntaxError, FileNotFoundException {
filename = inputFile.getAbsolutePath();
Lexer lexer = new Lexer(new FileReader(inputFile));

if (astFile != null) {
PrintStream ps = new PrintStream(new FileOutputStream(astFile));
System.setErr(ps);
}

Parser p = new Parser(lexer);

Symbol rtn;
try {
filename = inputFile.getAbsolutePath();
Lexer lexer = new Lexer(new FileReader(inputFile));

if (astFile != null) {
PrintStream ps = new PrintStream(new FileOutputStream(astFile));
System.setErr(ps);
}

Parser p = new Parser(lexer);

try {
rtn = p.parse();
} catch (SyntaxError se) {
throw se;
} catch (Exception e) {
throw new Error("Unexpected exception from parser");
}
if (astFile != null) {
System.setErr(System.err);
}
} catch (FileNotFoundException e) {
System.err.println("File not found: " + e.getMessage());
return null;
rtn = p.parse();
} catch (SyntaxError se) {
throw se;
} catch (Exception e) {
throw new Error("Unexpected exception from parser");
}
if (astFile != null) {
System.setErr(System.err);
}
return rtn;
}
Expand Down Expand Up @@ -227,7 +240,7 @@ nonterminal TrailerExpr trailer;
//nonterminal Setmaker setmaker;
// nonterminal Setmaker setmaker_sub;
// nonterminal ClassDef classdef;
nonterminal Call arglist;
nonterminal List<Expression> arglist, call_args;
nonterminal LabeledType labeledType, maybeLabeledType;
nonterminal ast.ClosureType closureType;
nonterminal List<LabeledType> throwsOpt;
Expand Down Expand Up @@ -269,7 +282,6 @@ nonterminal List<LabeledType> except_types;
nonterminal Throw throw_stmt;
nonterminal List<FunctionDef> constructors;
nonterminal FunctionDef constructor;
//nonterminal EndorseStatement endorse_stmt;
nonterminal EndorseIfStatement endorseIf_stmt;
nonterminal Call call_expr;
nonterminal Revert revert_stmt;
Expand Down Expand Up @@ -368,8 +380,14 @@ ipt_stmts ::=
ipt_stmt ::= ipt_name:a SEMI {:RESULT = a; :};

ipt_name ::= IMPORT:x STRING_LITERAL:a {:
RESULT = a;//new Import();
//RESULT.setLoc(new CodeLocation(xleft, xright, filename));
java.nio.file.Path path = java.nio.file.Paths.get((String) a);
if (!path.isAbsolute()) {
path = java.nio.file.Paths.get(filename).getParent().resolve(path);
}
if (!java.nio.file.Files.isRegularFile(path)) {
parser.reportError(aleft, aright, "imported file not found: " + a);
}
RESULT = a;
:};
//
//ipt_as_names ::=
Expand Down Expand Up @@ -666,10 +684,10 @@ plain_var_dec ::=
// RESULT.setLoc(new CodeLocation(aleft, aright, filename));
//
// :}
type:t NAME:a SEMI {:
maybeLabeledType:t NAME:a SEMI {:
Name name = new Name((String)a);
name.setLoc(new CodeLocation(aleft, aright, filename));
StateVariableDeclaration rnt = new StateVariableDeclaration(name, new LabeledType(t, null), null, false, false, false);
StateVariableDeclaration rnt = new StateVariableDeclaration(name, t, null, false, false, false);
RESULT = rnt;
RESULT.setLoc(new CodeLocation(aleft, aright, filename));
:};
Expand Down Expand Up @@ -1158,9 +1176,6 @@ stmt ::= assign_stmt:a {: RESULT = a; :}
| throw_stmt:a {: RESULT = a;:}
| revert_stmt:a {: RESULT = a;:}
| emit_stmt:a {: RESULT = a; :}
// | endorse_stmt:a {:
// RESULT = a;
// :}
| endorseIf_stmt:a {:
RESULT = a;
:}
Expand All @@ -1173,21 +1188,11 @@ stmt ::= assign_stmt:a {: RESULT = a; :}
:}
;

//endorse_stmt ::=
// ENDORSEIF:x LPAR name_list:exprList COMMA ifLabel:from RIGHT_ARROW ifLabel:to RPAR IN suite:s {:
// EndorseStatement statement = new EndorseStatement(exprList, from, to, s);
// RESULT = statement;
// RESULT.setLoc(new CodeLocation(xleft, xright, filename));
// :}
// ;

emit_stmt ::=
EMIT:x call_expr:e SEMI {:
if (!(e instanceof Call)) {
return null;
}

RESULT = new Emit((Call)e);
EMIT:x NAME:n call_args:a SEMI {:
Name event = new Name(n);
event.setLoc(new CodeLocation(nleft, nright, filename));
RESULT = new Emit(event, a);
RESULT.setLoc(new CodeLocation(xleft, xright, filename));
:}
;
Expand Down Expand Up @@ -1237,12 +1242,10 @@ atomic_stmt ::= ATOMIC:x suite:s exceptall_stmts:es {:
RESULT.setLoc(new CodeLocation(xleft, xright, filename));
:};

throw_stmt ::= THROW:x call_expr:e SEMI{:
if (!(e instanceof Call)) {
return null;
}

RESULT = new Throw((Call)e);
throw_stmt ::= THROW:x NAME:n call_args:a SEMI{:
Name exception = new Name(n);
exception.setLoc(new CodeLocation(nleft, nright, filename));
RESULT = new Throw(exception, a);
RESULT.setLoc(new CodeLocation(xleft, xright, filename));
:};

Expand Down Expand Up @@ -1594,9 +1597,9 @@ call_expr ::= trailer_expr:e LPAR RPAR transaction_spec:ts{:
RESULT = c;
RESULT.setLoc(new CodeLocation(eleft, eright, filename));
:}
| trailer_expr:e LPAR arglist:c RPAR transaction_spec:ts{:
c.setValue(e);
c.setSpec(ts);
| trailer_expr:e LPAR arglist:a RPAR transaction_spec:ts{:
Call c = new Call(e, a);
c.setSpec(ts);
RESULT = c;
RESULT.setLoc(new CodeLocation(eleft, eright, filename));
:}
Expand All @@ -1606,9 +1609,8 @@ call_expr ::= trailer_expr:e LPAR RPAR transaction_spec:ts{:
RESULT = c;
RESULT.setLoc(new CodeLocation(eleft, eright, filename));
:}
| trailer_expr:e LPAR arglist:c RPAR {:
c.setValue(e);
RESULT = c;
| trailer_expr:e LPAR arglist:a RPAR {:
RESULT = new Call(e, a);
RESULT.setLoc(new CodeLocation(eleft, eright, filename));
:}
| atom:a LPAR RPAR transaction_spec:ts {:
Expand All @@ -1624,15 +1626,14 @@ call_expr ::= trailer_expr:e LPAR RPAR transaction_spec:ts{:
RESULT = c;
RESULT.setLoc(new CodeLocation(aleft, aright, filename));
:}
| atom:a LPAR arglist:c RPAR transaction_spec:ts {:
c.setValue(a);
| atom:a LPAR arglist:l RPAR transaction_spec:ts {:
Call c = new Call(a, l);
c.setSpec(ts);
RESULT = c;
RESULT.setLoc(new CodeLocation(aleft, aright, filename));
:}
| atom:a LPAR arglist:c RPAR {:
c.setValue(a);
RESULT = c;
| atom:a LPAR arglist:l RPAR {:
RESULT = new Call(a, l);
RESULT.setLoc(new CodeLocation(aleft, aright, filename));
:}
;
Expand Down Expand Up @@ -1780,17 +1781,17 @@ trailer ::=
:};
arglist ::=
expr:a {:
//System.out.println("parsing first arg for arglist");
Call rnt = new Call();
rnt.addArg(a);
RESULT = rnt;
RESULT.setLoc(new CodeLocation(aleft, aright, filename));
List<Expression> rtn = new ArrayList<>();
rtn.add(a);
RESULT = rtn;
:}
| arglist:list COMMA expr:a {:
//System.out.println("parsing one more arg for arglist");
list.addArg(a);
list.add(a);
RESULT = list;
:};
call_args ::=
LPAR RPAR {: RESULT = new ArrayList<>(); :}
| LPAR arglist:a RPAR {: RESULT = a; :};
//exprlist ::=
// exprlist_sub:a {:RESULT = a;:}
// | exprlist_sub:a COMMA {:RESULT = a;:};
Expand Down
6 changes: 6 additions & 0 deletions src/SCIF.java
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,9 @@ public Integer call() {
} catch (TypeCheckFailure e) {
System.out.println(e.getMessage());
return 0;
} catch (java.io.FileNotFoundException e) {
System.out.println("File not found: " + e.getMessage());
return 1;
} catch (Exception e) {
System.out.println("Unexpected exception:");
e.printStackTrace();
Expand Down Expand Up @@ -218,6 +221,9 @@ public Integer call() {
Parser.parse(m_inputFiles[0], astOutputFile);
} catch (Parser.SyntaxError e) {
/* skip */
} catch (java.io.FileNotFoundException e) {
System.out.println("File not found: " + e.getMessage());
return 1;
}
} else if (m_funcRequest.tokenize) {
LexerTest.tokenize(m_inputFiles[0]);
Expand Down
Loading
Loading