From 5fd4b97399277c7d0f29878d680ea850a33a9e6e Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 28 Jun 2019 16:33:03 -0700 Subject: [PATCH] Adding new examples and tests: Groovy and Java programs. --- examples/BoundedBuffer.java | 143 ++++++++++++++++++++++++++++++ examples/BoundedBuffer.jpf | 4 + examples/ConcurrentCount.java | 59 ++++++++++++ examples/ConcurrentCount.jpf | 3 + examples/DiningPhil.java | 64 +++++++++++++ examples/DiningPhil.jpf | 3 + examples/NumericValueCheck.java | 31 +++++++ examples/NumericValueCheck.jpf | 10 +++ examples/Racer.groovy | 24 ----- examples/Rand.groovy | 6 +- examples/Rand.jpf | 2 +- examples/RandComplex.groovy | 28 ++++++ examples/RandComplex.jpf | 3 + examples/StopWatch.java | 35 ++++++++ examples/StopWatch.jpf | 3 + examples/TestExample-coverage.jpf | 7 ++ examples/TestExample.java | 74 ++++++++++++++++ 17 files changed, 471 insertions(+), 28 deletions(-) create mode 100644 examples/BoundedBuffer.java create mode 100644 examples/BoundedBuffer.jpf create mode 100644 examples/ConcurrentCount.java create mode 100644 examples/ConcurrentCount.jpf create mode 100644 examples/DiningPhil.java create mode 100644 examples/DiningPhil.jpf create mode 100644 examples/NumericValueCheck.java create mode 100644 examples/NumericValueCheck.jpf delete mode 100644 examples/Racer.groovy create mode 100644 examples/RandComplex.groovy create mode 100644 examples/RandComplex.jpf create mode 100644 examples/StopWatch.java create mode 100644 examples/StopWatch.jpf create mode 100644 examples/TestExample-coverage.jpf create mode 100644 examples/TestExample.java diff --git a/examples/BoundedBuffer.java b/examples/BoundedBuffer.java new file mode 100644 index 0000000..985fbc1 --- /dev/null +++ b/examples/BoundedBuffer.java @@ -0,0 +1,143 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +/** + * concurrency example with deadlock + * adapted from "Concurrency: State Models & Java Programs", Jeff Magee & Jeff Kramer + * + * Note there need to be at least 2x buffer_size instances of either producers or + * consumers in order to produce the deadlock, which basically depends on + * a notification choice between a consumer and a producer in a context where + * only threads of the notifier type are still runnable + * + * This is a good benchmark for state management/matching in a small heap context. + * Higher numbers of buffer size and producers/consumers result in a nice + * state explosion + */ +public class BoundedBuffer { + + static int BUFFER_SIZE = 1; + static int N_PRODUCERS = 4; + static int N_CONSUMERS = 4; + + static Object DATA = "fortytwo"; + + //--- the bounded buffer implementation + protected Object[] buf; + protected int in = 0; + protected int out= 0; + protected int count= 0; + protected int size; + + public BoundedBuffer(int size) { + this.size = size; + buf = new Object[size]; + } + + public synchronized void put(Object o) throws InterruptedException { + while (count == size) { + wait(); + } + buf[in] = o; + //System.out.println("PUT from " + Thread.currentThread().getName()); + ++count; + in = (in + 1) % size; + notify(); // if this is not a notifyAll() we might notify the wrong waiter + } + + public synchronized Object get() throws InterruptedException { + while (count == 0) { + wait(); + } + Object o = buf[out]; + buf[out] = null; + //System.out.println("GET from " + Thread.currentThread().getName()); + --count; + out = (out + 1) % size; + notify(); // if this is not a notifyAll() we might notify the wrong waiter + return (o); + } + + //--- the producer + static class Producer extends Thread { + static int nProducers = 1; + BoundedBuffer buf; + + Producer(BoundedBuffer b) { + buf = b; + setName("P" + nProducers++); + } + + @Override + public void run() { + try { + while(true) { + // to ease state matching, we don't put different objects in the buffer + buf.put(DATA); + } + } catch (InterruptedException e){} + } + } + + //--- the consumer + static class Consumer extends Thread { + static int nConsumers = 1; + BoundedBuffer buf; + + Consumer(BoundedBuffer b) { + buf = b; + setName( "C" + nConsumers++); + } + + @Override + public void run() { + try { + while(true) { + Object tmp = buf.get(); + } + } catch(InterruptedException e ){} + } + } + + //--- the test driver + public static void main(String [] args) { + readArguments( args); + //System.out.printf("running BoundedBuffer with buffer-size %d, %d producers and %d consumers\n", BUFFER_SIZE, N_PRODUCERS, N_CONSUMERS); + + BoundedBuffer buf = new BoundedBuffer(BUFFER_SIZE); + + for (int i=0; i 0){ + BUFFER_SIZE = Integer.parseInt(args[0]); + } + if (args.length > 1){ + N_PRODUCERS = Integer.parseInt(args[1]); + } + if (args.length > 2){ + N_CONSUMERS = Integer.parseInt(args[2]); + } + } +} diff --git a/examples/BoundedBuffer.jpf b/examples/BoundedBuffer.jpf new file mode 100644 index 0000000..bdd86dc --- /dev/null +++ b/examples/BoundedBuffer.jpf @@ -0,0 +1,4 @@ +target = BoundedBuffer + +# this should produce a deadlock +target.args = 2,4,1 \ No newline at end of file diff --git a/examples/ConcurrentCount.java b/examples/ConcurrentCount.java new file mode 100644 index 0000000..cedfd4e --- /dev/null +++ b/examples/ConcurrentCount.java @@ -0,0 +1,59 @@ +import java.util.concurrent.atomic.AtomicBoolean; + +public class ConcurrentCount { + static final int COUNT = 30000; + volatile static int count = COUNT; + volatile static AtomicBoolean lock = new AtomicBoolean(false); + static int a = 0; + static int b = 0; + + public static void main(String args[]) { + + new Thread() { + + @Override + public void run() { + while(count > 0) { + if (lock.get()) continue; + lock.set(true); + decreaseCount(); + a++; + lock.set(false); + + + } + } + }.start(); + + new Thread() { + + @Override + public void run() { + while(count > 0) { + if (lock.get()) continue; + lock.set(true); + decreaseCount(); + b++; + lock.set(false); + + + } + } + }.start(); + + while(count > 0); + //System.out.println("a = " + a); + //System.out.println("b = " + b); + //System.out.println("a + b = " + (a + b)); + //System.out.println("count = " + count); + + //Checks for concurrency error (which should be found when using model checking) + assert a + b == COUNT; + } + + private static synchronized void decreaseCount() { + count--; + } + +} + diff --git a/examples/ConcurrentCount.jpf b/examples/ConcurrentCount.jpf new file mode 100644 index 0000000..331cb24 --- /dev/null +++ b/examples/ConcurrentCount.jpf @@ -0,0 +1,3 @@ +listener=.listener.CGMonitor + +target = ConcurrentCount diff --git a/examples/DiningPhil.java b/examples/DiningPhil.java new file mode 100644 index 0000000..7295a5a --- /dev/null +++ b/examples/DiningPhil.java @@ -0,0 +1,64 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +public class DiningPhil { + + static class Fork { + } + + static class Philosopher extends Thread { + + Fork left; + Fork right; + + public Philosopher(Fork left, Fork right) { + this.left = left; + this.right = right; + //start(); + } + + @Override + public void run() { + // think! + synchronized (left) { + synchronized (right) { + // eat! + } + } + } + } + + static int nPhilosophers = 6; + + public static void main(String[] args) { + if (args.length > 0){ + nPhilosophers = Integer.parseInt(args[0]); + } + + //Verify.beginAtomic(); + Fork[] forks = new Fork[nPhilosophers]; + for (int i = 0; i < nPhilosophers; i++) { + forks[i] = new Fork(); + } + for (int i = 0; i < nPhilosophers; i++) { + Philosopher p = new Philosopher(forks[i], forks[(i + 1) % nPhilosophers]); + p.start(); + } + //Verify.endAtomic(); + } +} \ No newline at end of file diff --git a/examples/DiningPhil.jpf b/examples/DiningPhil.jpf new file mode 100644 index 0000000..901b818 --- /dev/null +++ b/examples/DiningPhil.jpf @@ -0,0 +1,3 @@ +target = DiningPhil + +search.class = .search.heuristic.BFSHeuristic diff --git a/examples/NumericValueCheck.java b/examples/NumericValueCheck.java new file mode 100644 index 0000000..d99f092 --- /dev/null +++ b/examples/NumericValueCheck.java @@ -0,0 +1,31 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +/** + * example to catch numeric value rnge violations with the NumericValueChecker listener + */ +public class NumericValueCheck { + + public static void main (String[] args){ + double someVariable; + + someVariable = 42; // what else + + someVariable = 12345; // ..That's the number only an idiot would have on his luggage + } +} diff --git a/examples/NumericValueCheck.jpf b/examples/NumericValueCheck.jpf new file mode 100644 index 0000000..6fa8a95 --- /dev/null +++ b/examples/NumericValueCheck.jpf @@ -0,0 +1,10 @@ +target = NumericValueCheck + +listener = .listener.NumericValueChecker + +# NumericValueChecker configuration +range.vars = 1 +range.1.var = NumericValueCheck.main(java.lang.String[]):someVariable +range.1.min = 0 +range.1.max = 42 + diff --git a/examples/Racer.groovy b/examples/Racer.groovy deleted file mode 100644 index e8df2f8..0000000 --- a/examples/Racer.groovy +++ /dev/null @@ -1,24 +0,0 @@ -class Racer implements Runnable { - int d = 42 - - public void run () { - doSomething(1001) - d = 0 // (1) - } - - static void main (String[] args){ - Racer racer = new Racer() - Thread t = new Thread(racer) - t.start() - - doSomething(1000) - int c = 420 / racer.d // (2) - println c - } - - def doSomething (int n) { - try { - Thread.sleep(n) - } catch (InterruptedException ix) {} - } -} diff --git a/examples/Rand.groovy b/examples/Rand.groovy index 4d6ff32..11b5caa 100644 --- a/examples/Rand.groovy +++ b/examples/Rand.groovy @@ -3,12 +3,12 @@ class Rand { println("Groovy model-checking") Random random = new Random(42); - int a = random.nextInt(2) - int b = random.nextInt(3) + int a = random.nextInt(10) + int b = random.nextInt(10) println("a=" + a) println(" b=" + b) - int c = a/(b+a -2) + int c = a/(b+a -5) println(" c=" + c) } } diff --git a/examples/Rand.jpf b/examples/Rand.jpf index 57cd211..e81cc62 100644 --- a/examples/Rand.jpf +++ b/examples/Rand.jpf @@ -1,3 +1,3 @@ target = Rand cg.enumerate_random = true -report.console.property_violation=error,trace +#report.console.property_violation=error,trace diff --git a/examples/RandComplex.groovy b/examples/RandComplex.groovy new file mode 100644 index 0000000..fc2d647 --- /dev/null +++ b/examples/RandComplex.groovy @@ -0,0 +1,28 @@ +// This function runs when the SmartApp is installed +def installed(a, b, c) { + println("a=" + a) + initialize(a, b, c) +} + +// This function is where you initialize callbacks for event listeners +def initialize(a, b, c) { + println(" b=" + b) + finalize(a, b, c) +} + +def finalize(a, b, c) { + println(" c=" + c) + result(a, b, c) +} + +def result(a, b, c) { + int d = a/(b+c-10) + println(" d=" + d) +} + +Random random = new Random(42) +int a = random.nextInt(10) +int b = random.nextInt(10) +int c = random.nextInt(10) +installed(a,b,c) +println "End of call!" \ No newline at end of file diff --git a/examples/RandComplex.jpf b/examples/RandComplex.jpf new file mode 100644 index 0000000..49d418d --- /dev/null +++ b/examples/RandComplex.jpf @@ -0,0 +1,3 @@ +target = RandComplex +cg.enumerate_random = true +#report.console.property_violation=error,trace diff --git a/examples/StopWatch.java b/examples/StopWatch.java new file mode 100644 index 0000000..8da5066 --- /dev/null +++ b/examples/StopWatch.java @@ -0,0 +1,35 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +/** + * example to show how to explore off-nominal paths + */ +public class StopWatch { + + public static void main(String[] args){ + long tStart = System.currentTimeMillis(); + System.out.println("some lengthy computation.."); + long tEnd = System.currentTimeMillis(); + + if (tEnd - tStart > 1000){ + throw new RuntimeException("it took too long.."); + } + + System.out.println("all fine, finished in time"); + } +} diff --git a/examples/StopWatch.jpf b/examples/StopWatch.jpf new file mode 100644 index 0000000..2cabef9 --- /dev/null +++ b/examples/StopWatch.jpf @@ -0,0 +1,3 @@ +target = StopWatch + +listener = .listener.StopWatchFuzzer diff --git a/examples/TestExample-coverage.jpf b/examples/TestExample-coverage.jpf new file mode 100644 index 0000000..75d9ed4 --- /dev/null +++ b/examples/TestExample-coverage.jpf @@ -0,0 +1,7 @@ +target = TestExample + +listener=.listener.CoverageAnalyzer + +coverage.include = T1,T2 +coverage.show_methods = true +#coverage.show_bodies = true \ No newline at end of file diff --git a/examples/TestExample.java b/examples/TestExample.java new file mode 100644 index 0000000..48aebdc --- /dev/null +++ b/examples/TestExample.java @@ -0,0 +1,74 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +class T1 { + int d = 42; + + public int func1(int a, int b) { + if (a > b) { + return 1; + } else if (a == b) { + return 0; + } else { + return -1; + } + } + + public boolean func2(boolean cond) { + if (cond && (d > 40)) { + d--; + } else { + d++; + } + return cond; + } +} + +class T2 { + + public int computeSomething (int a, int b){ + try { + return a / b; + } catch (ArithmeticException ax){ + return -1; // pretty lame error handling + } + } + + public void doSomething() { + System.out.println("something"); + } +} + +public class TestExample { + + public static void main(String[] args) { + T1 t1 = new T1(); + + assert t1.func1(1, 0) > 0; + assert t1.func1(0, 1) < 0; + + assert t1.func2(true) == true; + assert t1.func2(false) == false; + + + T2 t2 = new T2(); + + assert t2.computeSomething(42, 42) == 1.0; + } +} + -- 2.34.1