From d2ca5984f079111b851bf9f2a4618d5542a17c39 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 2 Jul 2020 20:44:25 -0700
Subject: [PATCH] Avoid rollover with long

---
 moreStatistics                                       |  4 ++++
 src/main/gov/nasa/jpf/vm/ElementInfo.java            |  6 +++---
 src/main/gov/nasa/jpf/vm/JPFOutputStream.java        |  2 +-
 src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java | 10 +++++-----
 4 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/moreStatistics b/moreStatistics
index 0b9af17..329e40d 100644
--- a/moreStatistics
+++ b/moreStatistics
@@ -2,3 +2,7 @@
 ==> DEBUG: Number of conflicts   : 4
 ==> DEBUG: Number of transitions : 7
 
+==> DEBUG: State reduction mode  : true
+==> DEBUG: Number of conflicts   : 4
+==> DEBUG: Number of transitions : 7
+
diff --git a/src/main/gov/nasa/jpf/vm/ElementInfo.java b/src/main/gov/nasa/jpf/vm/ElementInfo.java
index d853afb..c34e1c1 100644
--- a/src/main/gov/nasa/jpf/vm/ElementInfo.java
+++ b/src/main/gov/nasa/jpf/vm/ElementInfo.java
@@ -137,7 +137,7 @@ public abstract class ElementInfo implements Cloneable {
 
   // cache for a serialized representation of the object, which can be used
   // by state-matching. Value interpretation depends on the configured Serializer
-  protected int sid;
+  protected long sid;
 
 
   // helpers for state storage/restore processing, to avoid explicit iterators on
@@ -259,11 +259,11 @@ public abstract class ElementInfo implements Cloneable {
   
   
   //--- sids are only supposed to be used by the Serializer
-  public void setSid(int id){
+  public void setSid(long id){
     sid = id;
   }
 
-  public int getSid() {
+  public long getSid() {
     return sid;
   }
 
diff --git a/src/main/gov/nasa/jpf/vm/JPFOutputStream.java b/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
index 71dfb9f..9b4fbbe 100644
--- a/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
+++ b/src/main/gov/nasa/jpf/vm/JPFOutputStream.java
@@ -121,7 +121,7 @@ public class JPFOutputStream extends OutputStream {
     boolean isObject = ei.isObject();
     ClassInfo ci = ei.getClassInfo();
     
-    int ref = (useSid) ? ei.getSid() : ei.getObjectRef();
+    int ref = (useSid) ? ((int)ei.getSid()) : ei.getObjectRef();
     ps.printf("@%x ", ref);
     
     if (isObject){
diff --git a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
index 7b58177..0f6eb0e 100644
--- a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
@@ -55,8 +55,8 @@ public class CFSerializer extends FilteringSerializer {
   // over the serialized objects to reset their sids. This works by resetting
   // the sid to 0 upon backtrack, and counting either upwards from 1 or downwards
   // from -1, but store the absolute value in the serialization stream
-  int initsidCount=0;
-  int sidCount=1;
+  long initsidCount=0;
+  long sidCount=1;
 
   @Override
   protected void initReferenceQueue() {
@@ -83,7 +83,7 @@ public class CFSerializer extends FilteringSerializer {
         buf.add(0);
         return;
       }
-      int sid = ei.getSid();
+      long sid = ei.getSid();
       
       if (sid <= initsidCount){ // count sid upwards from 1
           sid = sidCount++;
@@ -92,7 +92,7 @@ public class CFSerializer extends FilteringSerializer {
       }
 
       // note that we always add the absolute sid value
-      buf.add(sid - initsidCount);
+      buf.add((int)(sid - initsidCount));
     }
   }
 
@@ -171,6 +171,6 @@ public class CFSerializer extends FilteringSerializer {
   
   @Override
   protected int getSerializedReferenceValue (ElementInfo ei){
-    return ei.getSid()-initsidCount;
+    return (int)(ei.getSid()-initsidCount);
   }
 }
-- 
2.34.1