work on artifact description

Author: ftc

implementation/ECOOP_AE_Submission_Document.md

@@ -21,8 +21,6 @@ ECOOP submission number for the paper: **303**
 
 Please describe how reviewers can check the artifact's integrity and basic functionality.
 
-TODO####!!!!!: test these on a different machine before submitting artifact.
-
 There are two docker containers, one for Wistoria and another for the Infer/Pulse comparison. 
 Separation of these containers was done to avoid dependency conflicts.
 Please test that both are working using the following instructions:
@@ -48,8 +46,20 @@ TODO####!!!!  add instructions here once c has script
 Please list for each distinct component of your artifact:
 
 * type of artifact (data, code, proof, etc.)
+  * Wistoria: Source code for Wistoria (based on the Historia implementation) 
+  * Benchmarks: Data in the form of the source code for the 9 benchmarks from the paper.
+  * CBCFTL specification: Data in the form of CBCFTL specifications used for the experiments.
+  * Recorded Traces: Data in the form of recorded runtime traces for each app.
 * format (e.g., CSV, source code, binary, etc.)
+  * Wistoria: Scala code
+  * Benchmarks: Java code, Android project config files, 
+  * CBCFTL specifications: Defined directly using the CBCFTL AST case classes in Scala code (no human-readable parser).
+  * Recorded Traces: text log files.
 * location in the container/VM
+  * Wistoria: `/home/bounder/`
+  * Benchmarks: `/home/testApps/ChatGPT_Benchmarks`. Each benchmark is in own directory corresponding to the names. The implementation is in `app_bug` subdirectory)
+  * CBCFTL: `/home/notebooks/reachExpGPT/ReachExpGPT.ipynb` and `/home/bounder/src/main/scala/edu/colorado/plv/bounder/lifestate/Specification.scala`
+  * Recorded Traces: May be found in the corresponding benchmark directory and are named `logcat.txt` or `logcat[n].txt` where n is some number.
 
 ## For authors claiming an available badge
 
@@ -70,6 +80,14 @@ For example: “The data in table 1 can be obtained by running script ‘generat
 
 Please note: we highly advise authors to provide a push-button evaluation (cf. call for artifacts).
 
+* Table 1:
+  * This is data that was obtained by manually counting and inspecting the applications in the Benchmarks directories mentioned earlier.
+* Table 2:
+  * This is a summary of the error condition in `ReachExpGPT.ipynb` and may be found as the variable `query` for each benchmark.
+* Table 3:
+  * After running the `ReachExpGPT.ipynb` notebook with  `Kernel -> Restart Kernel and Run All Cells...`
+  * Table 3 will be displayed under the header "Table 3 Producing Realistic Execution Histories"
+
 ## For authors claiming a reusable badge
 
 If some parts of your artifacts contains software:

notebooks/reachExpGPT/Bitmap/stdout.tct

@@ -1,32 +1 @@
 java.library.path set to: /usr/lib/:/usr/java/packages/lib:/usr/lib/x86_64-linux-gnu/jni:/lib/x86_64-linux-gnu:/usr/lib/x86_64-linux-gnu:/usr/lib/jni:/lib:/usr/lib
-remaining tasks: 1 / 2
-    ord depth: 0
-remaining tasks: 0 / 2
-    ord depth: 0
-    depth: 0
-    depth: 0
-    State: ( locals: @this -> p-0         heap:           pure:          types: List(p-0:{3963})    trace: )
-    State: ( locals: @this -> p-0         heap:           pure:          types: List(p-0:{3963})    trace: )
-    Loc  : pre-line: 55 return
-    Loc  : pre-line: 55 return
-    Method  : Some(JimpleMethodLoc(<com.example.configchange.MainActivity: void onDestroy()>))
-    Method  : Some(JimpleMethodLoc(<com.example.configchange.MainActivity: void onDestroy()>))
-remaining tasks: 0 / 1
-    ord depth: 2
-    depth: 39
-    State: ( locals: @this -> p-1         heap:           pure: p-0  !=  NULL         types: List(p-0:{3963}, p-1:{3963})    trace: O(CBExit I_CBExit_ActivityonCreate ( _T_,p-1 );O(CBEnter I_CBEnter_ActivityonDestroy ( _T_,p-0 ))
-    Loc  : post-line: 49 return
-    Method  : Some(JimpleMethodLoc(<com.example.configchange.MainActivity: void onCreate(android.os.Bundle)>))
-ecluded method: JimpleMethodLoc(<com.example.configchange.MainActivity: void dumpFields(java.lang.Object,java.lang.Class)>)
-!!!Found witness, terminating other processes.
-Writing trace 0 / 1, length: 233
-Writing trace 0 / 1, length: 37
-witness: 
- (    heap:           pure: p-0  !=  NULL && p-1  !=  NULL         types: List(p-0:{3963}, p-1:{3963})    trace: O(CBEnter I_CBEnter_ActivityonCreate ( _T_,p-1 );O(CBExit I_CBExit_ActivityonCreate ( _T_,p-1 );O(CBEnter I_CBEnter_ActivityonDestroy ( _T_,p-0 ))
-last state: 
- Future trace:
- CBEnter void onCreate(android.os.Bundle)( _T_,@2 )
-CBExit void onCreate(android.os.Bundle)( _T_,@2 )
-CBEnter void onDestroy()( _T_,@2 )
-
-analysis time(ms): 19346983059

notebooks/reachExpGPT/ConfigChange/stdout.tct

@@ -1,37 +1 @@
 java.library.path set to: /usr/lib/:/usr/java/packages/lib:/usr/lib/x86_64-linux-gnu/jni:/lib/x86_64-linux-gnu:/usr/lib/x86_64-linux-gnu:/usr/lib/jni:/lib:/usr/lib
-remaining tasks: 0 / 2
-    ord depth: 0
-    depth: 0
-remaining tasks: 1 / 2
-    ord depth: 0
-    depth: 0
-    State: ( locals: @this -> p-0         heap:           pure:          types: List(p-0:{1199})    trace: )
-    State: ( locals: @this -> p-0         heap:           pure:          types: List(p-0:{1199})    trace: )
-    Loc  : pre-line: 77 return
-    Loc  : pre-line: 77 return
-    Method  : Some(JimpleMethodLoc(<com.example.bitmapmishandle.MainActivity: void onDestroy()>))
-    Method  : Some(JimpleMethodLoc(<com.example.bitmapmishandle.MainActivity: void onDestroy()>))
-remaining tasks: 0 / 1
-    ord depth: 2
-    depth: 39
-    State: ( locals:          heap:           pure: p-0  !=  NULL         types: List(p-0:{1199})    trace: O(CBEnter I_CBEnter_ActivityonDestroy ( _T_,p-0 ))
-    Loc  : post-line: 71 return
-    Method  : Some(JimpleMethodLoc(<com.example.bitmapmishandle.MainActivity: void onCreate(android.os.Bundle)>))
-ecluded method: JimpleMethodLoc(<com.example.bitmapmishandle.MainActivity: void dumpFields(java.lang.Object,java.lang.Class)>)
-!!!Found witness, terminating other processes.
-Writing trace 0 / 1, length: 391
-Writing trace 0 / 1, length: 37
-witness: 
- (    heap:           pure: p-2  !=  NULL && p-3  !=  NULL && p-0  !=  NULL && p-1  !=  NULL         types: List(p-0:{1199}, p-1:{1213}, p-3:{1199}, p-2:{1207})    trace: O(CBEnter I_CBEnter_ActivityonCreate ( _T_,p-3 );p-2;O(CIExit I_CIExit_Dialoginit ( _T_,p-2,p-3 );O(CIExit I_CIExit_DialogsetMessage ( _T_,p-2,NULL );O(CIExit I_CIExit_Dialogshow ( _T_,_T_ );p-1;O(CIExit I_CIExit_Threadstart ( _T_,p-1 );O(CBEnter I_CBEnter_ActivityonDestroy ( _T_,p-0 ))
-last state: 
- Future trace:
- CBEnter void onCreate(android.os.Bundle)( _T_,@7 )
-TNew(@2,{1})
-CIExit  <init>(( _T_,@2,@7 )
-CIExit  setMessage(( _T_,@2,NULL )
-CIExit show(( _T_,_T_ )
-TNew(@4,{2})
-CIExit void start(( _T_,@4 )
-CBEnter void onDestroy()( _T_,@5 )
-
-analysis time(ms): 5986590275