From 86b219fc02f98e073ecd568a200ea86086bd5ee0 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 11 May 2016 19:44:02 +0200
Subject: [PATCH] use implicit state for random with correct execution

---
 library/leon/util/Random.scala                | 77 +++++++++++++++++--
 testcases/verification/xlang/DataRacing.scala |  3 +-
 2 files changed, 71 insertions(+), 9 deletions(-)

diff --git a/library/leon/util/Random.scala b/library/leon/util/Random.scala
index e8efac0bd..b6e60aa0a 100644
--- a/library/leon/util/Random.scala
+++ b/library/leon/util/Random.scala
@@ -7,30 +7,91 @@ import leon.lang.xlang._
 
 object Random {
 
+  @library
+  case class State(var seed: BigInt)
+
+  @library
+  def newState: State = State(0)
+
+
   @library
   @isabelle.noBody()
-  def nextBoolean(): Boolean = epsilon((x: Boolean) => true)
+  def nextBoolean(implicit state: State): Boolean = {
+    state.seed += 1
+    nativeNextBoolean
+  } ensuring((x: Boolean) => true)
 
   @library
+  @extern
   @isabelle.noBody()
-  def nextInt(): Int = epsilon((x: Int) => true)
+  private def nativeNextBoolean(implicit state: State): Boolean = {
+    scala.util.Random.nextBoolean
+  } ensuring((x: Boolean) => true)
+
+
+
+  @library
+  @isabelle.noBody()
+  def nextInt(implicit state: State): Int = {
+    state.seed += 1
+    nativeNextInt
+  } ensuring((x: Int) => true)
+
+  @library
+  @extern
+  @isabelle.noBody()
+  private def nativeNextInt(implicit state: State): Int = {
+    scala.util.Random.nextInt
+  } ensuring((x: Int) => true)
+
+
 
   @library
   @isabelle.noBody()
-  def nextInt(max: Int): Int = {
+  def nextInt(max: Int)(implicit state: State): Int = {
     require(max > 0)
-    epsilon((x: Int) => x >= 0 && x < max)
+    state.seed += 1
+    nativeNextInt(max)
   } ensuring(res => res >= 0 && res < max)
 
   @library
+  @extern
   @isabelle.noBody()
-  def nextBigInt(): BigInt = epsilon((x: BigInt) => true)
+  def nativeNextInt(max: Int)(implicit state: State): Int = {
+    scala.util.Random.nextInt(max)
+  } ensuring(res => res >= 0 && res < max)
+
+
+
+  @library
+  @isabelle.noBody()
+  def nextBigInt(implicit state: State): BigInt = {
+    state.seed += 1
+    nativeNextBigInt
+  } ensuring((x: BigInt) => true)
 
   @library
+  @extern
   @isabelle.noBody()
-  def nextBigInt(max: BigInt): BigInt = {
+  private def nativeNextBigInt(implicit state: State): BigInt = {
+    BigInt(scala.util.Random.nextInt)
+  } ensuring((x: BigInt) => true)
+
+
+
+  @library
+  @isabelle.noBody()
+  def nextBigInt(max: BigInt)(implicit state: State): BigInt = {
     require(max > 0)
-    epsilon((x: BigInt) => x >= 0 && x < max)
-  } ensuring(res => res >= 0 && res < max)
+    state.seed += 1
+    nativeNextBigInt(max)
+  } ensuring((res: BigInt) => res >= 0 && res < max)
+
+  @library
+  @extern
+  @isabelle.noBody()
+  private def nativeNextBigInt(max: BigInt)(implicit state: State): BigInt = {
+    BigInt(scala.util.Random.nextInt(max.toInt))
+  } ensuring((x: BigInt) => x >= 0 && x < max)
 
 }
diff --git a/testcases/verification/xlang/DataRacing.scala b/testcases/verification/xlang/DataRacing.scala
index f57640061..f709c2be6 100644
--- a/testcases/verification/xlang/DataRacing.scala
+++ b/testcases/verification/xlang/DataRacing.scala
@@ -16,7 +16,7 @@ object DataRacing {
   case class RunnableCons(instr: AtomicInstr, tail: Runnable) extends Runnable
   case class RunnableNil() extends Runnable
 
-  def execute(t1: Runnable, t2: Runnable, state: SharedState): Unit = (t1, t2) match {
+  def execute(t1: Runnable, t2: Runnable, state: SharedState)(implicit randomState: Random.State): Unit = (t1, t2) match {
     case (RunnableCons(x,xs), RunnableCons(y,ys)) =>
       if(Random.nextBoolean) {
         x.instr(state)
@@ -37,6 +37,7 @@ object DataRacing {
   //z3 finds counterexample in 0.5
   //cvc4 needs 130 seconds
   def main(): Int = {
+    implicit val randomState = Random.newState
     val state = SharedState(0)
     val t1 = RunnableCons((s: SharedState) => s.i = s.i + 1, RunnableNil())
     val t2 = RunnableCons((s: SharedState) => s.i = s.i * 2, RunnableNil())
-- 
GitLab