Skip to content

Commit

Permalink
Setup 0.10.3
Browse files Browse the repository at this point in the history
  • Loading branch information
michbarsinai committed Mar 30, 2019
2 parents f8718eb + b8c2d92 commit 27cad35
Show file tree
Hide file tree
Showing 24 changed files with 619 additions and 88 deletions.
13 changes: 13 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,19 @@ a link to this page somewhere in the documentation/system about section.

## Change Log for the BPjs Library.

### 2019-03-30
* :arrow_up: Improved state hashing
* :arrow_up: More tests for the verifier
* :sparkles: Proper JavaScript error reporting at runtime (e.g. invoking methods of `null`). (#52)
* :sparkles: Proper JavaScript error reporting at for verification. To this end, a new violation, `JSErrorViolation`, was added. (#79)
* :arrow_up: Updated error message when calling `bp.sync` from a non-b-thread context.

### 2019-03-29
* :bug: Fixed a bug in the verifier, where a non-cyclic path ending in a visited node is not inspected.
* :bug: Hash code fixes.
* :arrow_up: Interface cleanups in the DfsBProgramVerifier: some method exposed the internal DFS nodes, and now they don't do that anymore.
* :arrow_up: More tests

### 2019-03-10
* :put_litter_in_its_place: Code cleanup.

Expand Down
19 changes: 15 additions & 4 deletions dependency-reduced-pom.xml
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@
<groupId>com.github.bthink-bgu</groupId>
<artifactId>BPjs</artifactId>
<name>BPjs</name>
<version>0.10.1</version>
<description>Provides a runtime for behavioral programs written in Javascript. It can
run stand-alone (from the commmandline) or be embedded in larger
JVM-based systems.</description>
<version>0.10.2</version>
<description>Provides runtime and analysis for behavioral programs written in
JavaScript. It can run stand-alone (from the commmandline) or be
embedded in larger JVM-based systems.</description>
<url>https://github.com/bThink-BGU/</url>
<developers>
<developer>
Expand Down Expand Up @@ -67,6 +67,17 @@
</archive>
</configuration>
</plugin>
<plugin>
<artifactId>maven-jar-plugin</artifactId>
<version>3.1.1</version>
<configuration>
<archive>
<manifest>
<mainClass>il.ac.bgu.cs.bp.bpjs.mains.BPJsCliRunner</mainClass>
</manifest>
</archive>
</configuration>
</plugin>
</plugins>
</build>
<profiles>
Expand Down
2 changes: 1 addition & 1 deletion pom.xml
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@

<groupId>com.github.bthink-bgu</groupId>
<artifactId>BPjs</artifactId>
<version>0.10.2</version>
<version>0.10.3</version>
<packaging>jar</packaging>

<name>BPjs</name>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,9 @@
*/
package il.ac.bgu.cs.bp.bpjs.analysis;

import il.ac.bgu.cs.bp.bpjs.analysis.violations.JsErrorViolation;
import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation;
import il.ac.bgu.cs.bp.bpjs.exceptions.BPjsRuntimeException;
import java.util.ArrayList;
import java.util.List;

Expand Down Expand Up @@ -86,7 +88,7 @@ public static interface ProgressListener {
* @param vfr The verifier.
* @see DfsBProgramVerifier#setMaxTraceLength(long)
*/
void maxTraceLengthHit(List<DfsTraversalNode> aTrace, DfsBProgramVerifier vfr);
void maxTraceLengthHit(ExecutionTrace aTrace, DfsBProgramVerifier vfr);

/**
* Verifier {@code vfr} reports a found violation. It is up to the listener
Expand All @@ -107,10 +109,10 @@ public static interface ProgressListener {
void done(DfsBProgramVerifier vfr);
}

private static class ViolatingCycleFoundException extends Exception{
private static class ViolatingPathFoundException extends Exception {
final Violation v;

public ViolatingCycleFoundException(Violation v) {
public ViolatingPathFoundException(Violation v) {
this.v = v;
}
}
Expand All @@ -122,7 +124,7 @@ public ViolatingCycleFoundException(Violation v) {
private static final ProgressListener NULL_PROGRESS_LISTENER = new ProgressListener() {
@Override public void started(DfsBProgramVerifier vfr) {}
@Override public void iterationCount(long count, long statesHit, DfsBProgramVerifier vfr) {}
@Override public void maxTraceLengthHit(List<DfsTraversalNode> aTrace, DfsBProgramVerifier vfr) {}
@Override public void maxTraceLengthHit(ExecutionTrace aTrace, DfsBProgramVerifier vfr) {}
@Override public void done(DfsBProgramVerifier vfr) {}

@Override
Expand Down Expand Up @@ -186,7 +188,7 @@ protected Violation dfsUsingStack(DfsTraversalNode aStartNode, ExecutorService e

if (pathLength() == maxTraceLength) {
// fold stack;
listener.maxTraceLengthHit(currentPath, this);
listener.maxTraceLengthHit(trace, this);
pop();

} else {
Expand All @@ -211,7 +213,7 @@ protected Violation dfsUsingStack(DfsTraversalNode aStartNode, ExecutorService e
v = inspectCurrentTrace();
if ( v != null ) return v;
}
} catch (ViolatingCycleFoundException vcfe ) {
} catch (ViolatingPathFoundException vcfe ) {
return vcfe.v;
}
}
Expand All @@ -224,34 +226,59 @@ protected Violation dfsUsingStack(DfsTraversalNode aStartNode, ExecutorService e
return null;
}

protected DfsTraversalNode getUnvisitedNextNode(DfsTraversalNode src, ExecutorService execSvc) throws ViolatingCycleFoundException, Exception {
protected DfsTraversalNode getUnvisitedNextNode(DfsTraversalNode src, ExecutorService execSvc)
throws ViolatingPathFoundException{
while (src.getEventIterator().hasNext()) {
final BEvent nextEvent = src.getEventIterator().next();
DfsTraversalNode possibleNextNode = src.getNextNode(nextEvent, execSvc);
visitedEdgeCount++;

BProgramSyncSnapshot pns = possibleNextNode.getSystemState();
if (visited.isVisited(pns) ) {
// Found a possible cycle

for ( int idx=0; idx<currentPath.size(); idx++) {
DfsTraversalNode nd = currentPath.get(idx);
if ( pns.equals(nd.getSystemState()) ) {
// found an actual cycle
trace.cycleTo(nextEvent, idx);
try {
DfsTraversalNode possibleNextNode = src.getNextNode(nextEvent, execSvc);
visitedEdgeCount++;

BProgramSyncSnapshot pns = possibleNextNode.getSystemState();
if (visited.isVisited(pns) ) {
boolean cycleFound = false;
for ( int idx=0; idx<currentPath.size() && !cycleFound; idx++) {
// Was this a cycle?
DfsTraversalNode nd = currentPath.get(idx);
if ( pns.equals(nd.getSystemState()) ) {
// found an actual cycle
cycleFound = true;
trace.cycleTo(nextEvent, idx);
Set<Violation> res = inspections.stream().map(i->i.inspectTrace(trace))
.filter(o->o.isPresent()).map(Optional::get).collect(toSet());

for ( Violation v : res ) {
if ( ! listener.violationFound(v, this)) {
throw new ViolatingPathFoundException(v);
}
}
}
}
if ( ! cycleFound ) {
// revisiting a state from a different path. Quickly inspect the path and contnue.
trace.advance(nextEvent, pns);
Set<Violation> res = inspections.stream().map(i->i.inspectTrace(trace))
.filter(o->o.isPresent()).map(Optional::get).collect(toSet());

for ( Violation v : res ) {
if ( ! listener.violationFound(v, this)) {
throw new ViolatingCycleFoundException(v);
.filter(o->o.isPresent()).map(Optional::get).collect(toSet());
if ( res.size() > 0 ) {
for ( Violation v : res ) {
if ( ! listener.violationFound(v, this) ) {
throw new ViolatingPathFoundException(v);
}
}
}
trace.pop();
}
}
} else {
// advance to this newly discovered node
return possibleNextNode;
} else {
// advance to this newly discovered node
return possibleNextNode;
}
} catch ( BPjsRuntimeException bprte ) {
trace.advance(nextEvent, null);
Violation jsev = new JsErrorViolation(trace, bprte);
if ( ! listener.violationFound(jsev, this) ) {
throw new ViolatingPathFoundException(jsev);
}
trace.pop();
}
}
return null;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package il.ac.bgu.cs.bp.bpjs.analysis;

import il.ac.bgu.cs.bp.bpjs.bprogramio.BProgramSyncSnapshotCloner;
import il.ac.bgu.cs.bp.bpjs.exceptions.BPjsRuntimeException;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Iterator;
Expand Down Expand Up @@ -82,10 +83,14 @@ public String toString() {
* @param exSvc The executor service that will run the threads
* @return State of the BProgram after event {@code e} was selected while
* the program was at {@code this} node's state.
* @throws Exception In case there's an error running the JavaScript code.
* @throws BPjsRuntimeException In case there's an error running the JavaScript code.
*/
public DfsTraversalNode getNextNode(BEvent e, ExecutorService exSvc) throws Exception {
return new DfsTraversalNode(bp, BProgramSyncSnapshotCloner.clone(systemState).triggerEvent(e, exSvc, Collections.emptySet()), e);
public DfsTraversalNode getNextNode(BEvent e, ExecutorService exSvc) throws BPjsRuntimeException {
try {
return new DfsTraversalNode(bp, BProgramSyncSnapshotCloner.clone(systemState).triggerEvent(e, exSvc, Collections.emptySet()), e);
} catch ( InterruptedException ie ) {
throw new BPjsRuntimeException("Thread interrupted during event invocaiton", ie);
}
}

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,11 +23,10 @@
*/
package il.ac.bgu.cs.bp.bpjs.analysis.listeners;

import il.ac.bgu.cs.bp.bpjs.analysis.DfsTraversalNode;
import il.ac.bgu.cs.bp.bpjs.analysis.DfsBProgramVerifier;
import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace;
import il.ac.bgu.cs.bp.bpjs.analysis.violations.Violation;
import java.io.PrintStream;
import java.util.List;

/**
* Logs the state of the verifier with short, not too-detailed messages.
Expand Down Expand Up @@ -57,7 +56,7 @@ public void iterationCount(long count, long statesHit, DfsBProgramVerifier v) {
}

@Override
public void maxTraceLengthHit(List<DfsTraversalNode> trace, DfsBProgramVerifier v) {
public void maxTraceLengthHit(ExecutionTrace trace, DfsBProgramVerifier v) {
out.println("/v/ " + v.getCurrentBProgram().getName() + ": hit max trace length.");
}

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
/*
* The MIT License
*
* Copyright 2019 michael.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in
* all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
* THE SOFTWARE.
*/
package il.ac.bgu.cs.bp.bpjs.analysis.violations;

import il.ac.bgu.cs.bp.bpjs.analysis.ExecutionTrace;
import il.ac.bgu.cs.bp.bpjs.exceptions.BPjsRuntimeException;

/**
*
* @author michael
*/
public class JsErrorViolation extends Violation {

private final BPjsRuntimeException exception;

public JsErrorViolation(ExecutionTrace counterExampleTrace, BPjsRuntimeException anException) {
super(counterExampleTrace);
exception = anException;
}

@Override
public String decsribe() {
return "Runtime JavaScript Error: " + exception.getMessage();
}

public BPjsRuntimeException getThrownException() {
return exception;
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
*/
package il.ac.bgu.cs.bp.bpjs.execution;

import il.ac.bgu.cs.bp.bpjs.exceptions.BPjsRuntimeException;
import il.ac.bgu.cs.bp.bpjs.model.BProgram;
import il.ac.bgu.cs.bp.bpjs.model.BProgramSyncSnapshot;
import il.ac.bgu.cs.bp.bpjs.model.BEvent;
Expand Down Expand Up @@ -147,7 +148,8 @@ public void run() {
} else {
listeners.forEach(l->l.ended(bprog));
}

} catch ( BPjsRuntimeException bre ) {
listeners.forEach( l -> l.error(bprog, bre));
} catch (InterruptedException itr) {
System.err.println("BProgramRunner interrupted: " + itr.getMessage() );

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,7 @@ public void setInterruptHandler( Object aPossibleHandler ) {
}

////////////////////////
// sync ("bsync") related code
// sync ("bp.sync") related code

@Override
public void sync( NativeObject jsRWB, Object data ) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,18 @@ public interface BProgramRunnerListener {
*/
void eventSelected( BProgram bp, BEvent theEvent );

/**
* Called when the b-program code makes an error, e.g. attempts to invoke
* methods on {@code null}.
* @param bp the offending b-program
* @param ex the exception that was thrown because of the offense.
*/
default void error( BProgram bp, Exception ex ) {
System.err.println("JavaScript Error during program execution: " + ex.getMessage() );
System.err.println("Trace: ");
ex.printStackTrace(System.err);
}

/**
* Called when the b-program was halted.
* @param bp the b-program that was halted.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -65,5 +65,10 @@ public void eventSelected(BProgram bp, BEvent theEvent) {}

@Override
public void halted(BProgram bp) {}


@Override
public void error(BProgram bp, Exception ex) {
BProgramRunnerListener.super.error(bp, ex);
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,7 @@ private void logScriptExceptionAndQuit(EvaluatorException ee, String arg) {
println("General statistics:");
println(String.format("Time:\t%,d (msec)", res.getTimeMillies()));
println(String.format("States scanned:\t%,d", res.getScannedStatesCount()));
println(String.format("Edges scanned:\t%,d", res.getScannedEdgesCount()));


} catch ( Exception e ) {
Expand Down
2 changes: 1 addition & 1 deletion src/main/java/il/ac/bgu/cs/bp/bpjs/model/BEvent.java
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ public boolean equals(Object obj) {

@Override
public int hashCode() {
return name.hashCode() ^ getDataField().map(ScriptableUtils::jsHash).orElse(0);
return 19*name.hashCode() ^ getDataField().map(ScriptableUtils::jsHash).orElse(0);
}

@Override
Expand Down
Loading

0 comments on commit 27cad35

Please sign in to comment.