jpf-core.git
16 months agoadd extra methods cfbugfix
Brian Demsky [Sat, 4 Jul 2020 00:00:57 +0000 (17:00 -0700)]
add extra methods

16 months agoAvoid rollover with long
Brian Demsky [Fri, 3 Jul 2020 03:44:25 +0000 (20:44 -0700)]
Avoid rollover with long

16 months agoBug fix for CFSerializer
Brian Demsky [Fri, 3 Jul 2020 03:35:18 +0000 (20:35 -0700)]
Bug fix for CFSerializer

16 months agoFixing a bug: in the second round of boolean CG, we might encounter states in the...
rtrimana [Thu, 2 Jul 2020 22:31:13 +0000 (15:31 -0700)]
Fixing a bug: in the second round of boolean CG, we might encounter states in the first round that are considered new states; adding a guard condition for a map read.

17 months agoAdding debug mode guards for all main methods.
rtrimana [Fri, 26 Jun 2020 22:30:12 +0000 (15:30 -0700)]
Adding debug mode guards for all main methods.

17 months agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Mon, 22 Jun 2020 23:57:40 +0000 (16:57 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

17 months agoAdding a way for JPF to be informed that this is DPOR; otherwise number the hacked...
rtrimana [Mon, 22 Jun 2020 23:57:06 +0000 (16:57 -0700)]
Adding a way for JPF to be informed that this is DPOR; otherwise number the hacked number CGs only work for DPOR and it creates an infinite loop for a normal execution without DPOR.

17 months agoCommenting out a line that causes a lot of loops; let the exclusion trace continue...
rtrimana [Mon, 22 Jun 2020 02:53:09 +0000 (19:53 -0700)]
Commenting out a line that causes a lot of loops; let the exclusion trace continue to build up.

17 months agoBug fix: when state is not found in rGraph, that means the state is being visited...
rtrimana [Fri, 19 Jun 2020 18:50:50 +0000 (11:50 -0700)]
Bug fix: when state is not found in rGraph, that means the state is being visited and this is a loop (self-predecessor).

17 months agoA few hacks to make the list circular: this lets the CG not signal the JPF that the...
rtrimana [Fri, 19 Jun 2020 16:42:07 +0000 (09:42 -0700)]
A few hacks to make the list circular: this lets the CG not signal the JPF that the end of the list is the end of the CG execution.

17 months agoExplored trace needs to be constructed and modified as there are predecessor branches.
rtrimana [Wed, 17 Jun 2020 23:17:20 +0000 (16:17 -0700)]
Explored trace needs to be constructed and modified as there are predecessor branches.

17 months agoRenaming a variable.
rtrimana [Wed, 17 Jun 2020 20:55:17 +0000 (13:55 -0700)]
Renaming a variable.

17 months agoFixing a bug in isConflict method.
rtrimana [Wed, 17 Jun 2020 18:25:42 +0000 (11:25 -0700)]
Fixing a bug in isConflict method.

17 months agoMaking field exclusion checks more efficient.
rtrimana [Sat, 13 Jun 2020 22:50:31 +0000 (15:50 -0700)]
Making field exclusion checks more efficient.

17 months agoCommitting main.jpf.
rtrimana [Wed, 10 Jun 2020 16:39:04 +0000 (09:39 -0700)]
Committing main.jpf.

17 months agoFurther cleaning up (naming, comments, etc.).
rtrimana [Wed, 10 Jun 2020 16:11:54 +0000 (09:11 -0700)]
Further cleaning up (naming, comments, etc.).

17 months agoAdding happens-before push back.
rtrimana [Tue, 9 Jun 2020 21:24:37 +0000 (14:24 -0700)]
Adding happens-before push back.

17 months agoCleaning up.
rtrimana [Tue, 9 Jun 2020 19:08:07 +0000 (12:08 -0700)]
Cleaning up.

17 months agoNew algorithm implementation; without pushing forward hb transaction; untested/undebu...
rtrimana [Fri, 5 Jun 2020 20:45:40 +0000 (13:45 -0700)]
New algorithm implementation; without pushing forward hb transaction; untested/undebugged yet.

18 months agoAdding different main.jpf files for different detections.
rtrimana [Thu, 21 May 2020 18:27:06 +0000 (11:27 -0700)]
Adding different main.jpf files for different detections.

18 months agoEditing main.jpf
rtrimana [Thu, 21 May 2020 18:19:14 +0000 (11:19 -0700)]
Editing main.jpf

18 months agoAdding a script to set the environment variables for groovyc.
rtrimana [Thu, 21 May 2020 18:12:50 +0000 (11:12 -0700)]
Adding a script to set the environment variables for groovyc.

18 months agoFixing a bug: need to get the right choice/event number for IntIntervalGenerator...
rtrimana [Tue, 19 May 2020 16:38:08 +0000 (09:38 -0700)]
Fixing a bug: need to get the right choice/event number for IntIntervalGenerator CGs.

18 months agoTested updating backtrack sets in the reachability graph.
rtrimana [Fri, 15 May 2020 23:27:23 +0000 (16:27 -0700)]
Tested updating backtrack sets in the reachability graph.

18 months agoTested backtrack in a cycle (local).
rtrimana [Fri, 15 May 2020 19:31:39 +0000 (12:31 -0700)]
Tested backtrack in a cycle (local).

18 months agoAdjusting support methods for reachability analysis with the new algorithm; untested...
rtrimana [Thu, 14 May 2020 23:36:02 +0000 (16:36 -0700)]
Adjusting support methods for reachability analysis with the new algorithm; untested yet.

18 months agoModifying the algorithm: 1) Find the first conflict and stop; 2) Perform backward...
rtrimana [Thu, 14 May 2020 21:03:40 +0000 (14:03 -0700)]
Modifying the algorithm: 1) Find the first conflict and stop; 2) Perform backward DFS to find conflicts in the execution graph.

18 months agoFixing a bug: completing reachability graph with missing past traces.
rtrimana [Thu, 7 May 2020 18:14:42 +0000 (11:14 -0700)]
Fixing a bug: completing reachability graph with missing past traces.

18 months agoFixing bugs: state to reachability graph map has to be updated for every new state...
rtrimana [Sat, 2 May 2020 15:25:49 +0000 (08:25 -0700)]
Fixing bugs: state to reachability graph map has to be updated for every new state in the stateAdvanced method.

18 months agoAdding reachability graph for past executions.
rtrimana [Fri, 1 May 2020 22:47:12 +0000 (15:47 -0700)]
Adding reachability graph for past executions.

19 months agoAdditional logging feature.
rtrimana [Mon, 20 Apr 2020 19:29:48 +0000 (12:29 -0700)]
Additional logging feature.

19 months agoFixing a bug: mapping state to event has to be done after the execution termination...
rtrimana [Thu, 16 Apr 2020 21:44:45 +0000 (14:44 -0700)]
Fixing a bug: mapping state to event has to be done after the execution termination check, otherwise we stop too early.

19 months agoFixing more bugs with the reachability analysis.
rtrimana [Wed, 15 Apr 2020 23:34:11 +0000 (16:34 -0700)]
Fixing more bugs with the reachability analysis.

19 months agoFixing more potential bugs for the reachability analysis.
rtrimana [Wed, 15 Apr 2020 19:11:07 +0000 (12:11 -0700)]
Fixing more potential bugs for the reachability analysis.

19 months agoFixing a bug: separating the state tracking for cycle analysis.
rtrimana [Wed, 15 Apr 2020 06:53:59 +0000 (23:53 -0700)]
Fixing a bug: separating the state tracking for cycle analysis.

19 months agoAdding reachability analysis when state matching occurs.
rtrimana [Tue, 14 Apr 2020 23:24:10 +0000 (16:24 -0700)]
Adding reachability analysis when state matching occurs.

19 months agoModifying main.jpf
rtrimana [Mon, 13 Apr 2020 20:16:26 +0000 (13:16 -0700)]
Modifying main.jpf

19 months agoAdding a counter for number of conflicts.
rtrimana [Sun, 12 Apr 2020 07:21:43 +0000 (00:21 -0700)]
Adding a counter for number of conflicts.

19 months agoPrinting out the number of transitions.
rtrimana [Sat, 11 Apr 2020 21:26:46 +0000 (14:26 -0700)]
Printing out the number of transitions.

19 months agoFixing a bug: misunderstood how the VOD graph is supposed to be generated; we basical...
rtrimana [Fri, 10 Apr 2020 22:29:50 +0000 (15:29 -0700)]
Fixing a bug: misunderstood how the VOD graph is supposed to be generated; we basically track the transitions that produce new states.

19 months agoTesting DPORStateReducer and ConflictTracker: JPF seems to work fine and find the...
rtrimana [Thu, 9 Apr 2020 23:44:57 +0000 (16:44 -0700)]
Testing DPORStateReducer and ConflictTracker: JPF seems to work fine and find the conflicts.

19 months agoFixing a bug: java LinkedList needs removeFirst(), not getFirst() to get and remove...
rtrimana [Thu, 9 Apr 2020 23:29:40 +0000 (16:29 -0700)]
Fixing a bug: java LinkedList needs removeFirst(), not getFirst() to get and remove a node from the queue.

19 months agoFixing a bug: VOD graph traversal should continue with the next neighbor when there...
rtrimana [Thu, 9 Apr 2020 23:18:40 +0000 (16:18 -0700)]
Fixing a bug: VOD graph traversal should continue with the next neighbor when there is a loop (repeated node found).

19 months agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Thu, 9 Apr 2020 22:57:20 +0000 (15:57 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

19 months agoFixing a bug: restorable state has to be saved when backtrack point info is saved...
rtrimana [Thu, 9 Apr 2020 22:57:06 +0000 (15:57 -0700)]
Fixing a bug: restorable state has to be saved when backtrack point info is saved to get the appropriate CG type when restoring.

19 months agoOptimization: Compare just the state and the fist event/choice of the trace to not...
rtrimana [Thu, 9 Apr 2020 16:40:28 +0000 (09:40 -0700)]
Optimization: Compare just the state and the fist event/choice of the trace to not repeat the same backtrack trace twice (the two will map to the same state and the algorithm will stop the second execution, so there is no need to record and explore it twice, e.g., the traces 2 0 1 3 and 2 1 0 3 at state 3.

19 months agoChanging approach: Using vm.restoreState() method to restore JPF to the desired state...
rtrimana [Thu, 9 Apr 2020 07:03:43 +0000 (00:03 -0700)]
Changing approach: Using vm.restoreState() method to restore JPF to the desired state when backtracking; everything looks correct but probably needs more tests.

19 months agoCommitting a version that almost works: bug to fix is that when an execution finishes...
rtrimana [Wed, 8 Apr 2020 21:30:55 +0000 (14:30 -0700)]
Committing a version that almost works: bug to fix is that when an execution finishes and the first backtrack point requires to get back to a higher state, there is no mechanism to roll back to that state.

19 months agoFirst part of boolean flip seems to be clean; need to debug the second part and figur...
rtrimana [Tue, 7 Apr 2020 23:53:36 +0000 (16:53 -0700)]
First part of boolean flip seems to be clean; need to debug the second part and figure out what to do when the current state is lower than the highest state ID for backtrack.

19 months agoFixing a potential bug: we now store the event number in the ArrayList together with...
rtrimana [Tue, 7 Apr 2020 17:31:21 +0000 (10:31 -0700)]
Fixing a potential bug: we now store the event number in the ArrayList together with the list of CGs for backtracking; getting the event number directly from the current array might be misleading because the array choices might have been modified for fair-scheduling.

19 months agoCleaning up and fixing bugs; new DPOR implementation seems to be correct; need to...
rtrimana [Mon, 6 Apr 2020 23:31:08 +0000 (16:31 -0700)]
Cleaning up and fixing bugs; new DPOR implementation seems to be correct; need to test with other pairs.

19 months agoFixing a bug: we need to start choiceCounter from 1 instead of 0 for subsequent execu...
rtrimana [Sat, 4 Apr 2020 04:34:28 +0000 (21:34 -0700)]
Fixing a bug: we need to start choiceCounter from 1 instead of 0 for subsequent executions since the first CG (number 0) is the backtrack CG itself.

19 months agoReimplementing DPOR Phase 3: Architecting the subsequent executions (backtrack points...
rtrimana [Fri, 3 Apr 2020 23:13:34 +0000 (16:13 -0700)]
Reimplementing DPOR Phase 3: Architecting the subsequent executions (backtrack points); need to test how CGs are explored with the current DFSearch.

19 months agoReimplementing DPOR Phase 2: VOD graph building and traversal; completing R/W and...
rtrimana [Thu, 2 Apr 2020 23:20:26 +0000 (16:20 -0700)]
Reimplementing DPOR Phase 2: VOD graph building and traversal; completing R/W and conflict analysis; cleaning up and refactoring.

19 months agoReimplementing DPOR Phase 1: First trace execution, cycle detection, R/W field access...
rtrimana [Wed, 1 Apr 2020 23:44:57 +0000 (16:44 -0700)]
Reimplementing DPOR Phase 1: First trace execution, cycle detection, R/W field access analysis.

19 months agoStarting a new DPOR implementation.
rtrimana [Wed, 1 Apr 2020 18:20:05 +0000 (11:20 -0700)]
Starting a new DPOR implementation.

19 months agoCleaning up and refactoring.
rtrimana [Wed, 1 Apr 2020 18:09:26 +0000 (11:09 -0700)]
Cleaning up and refactoring.

19 months agoFixing bugs: capturing object accesses (read/write) in iterators.
rtrimana [Tue, 31 Mar 2020 23:25:00 +0000 (16:25 -0700)]
Fixing bugs: capturing object accesses (read/write) in iterators.

20 months agoFixing a bug: off-by-one error in the executed trace checking.
rtrimana [Fri, 27 Mar 2020 23:49:04 +0000 (16:49 -0700)]
Fixing a bug: off-by-one error in the executed trace checking.

20 months agoRe-checking and cleaning up the code: most likely still have a bug in re-ordering...
rtrimana [Fri, 27 Mar 2020 22:55:00 +0000 (15:55 -0700)]
Re-checking and cleaning up the code: most likely still have a bug in re-ordering the two apps.

20 months agoAdding the old tracker variable for debugging/testing purposes.
rtrimana [Thu, 26 Mar 2020 18:52:49 +0000 (11:52 -0700)]
Adding the old tracker variable for debugging/testing purposes.

20 months agoFixing bugs and cleaning up: Continuing sub-graph executions when there is no matched...
rtrimana [Thu, 26 Mar 2020 01:56:27 +0000 (18:56 -0700)]
Fixing bugs and cleaning up: Continuing sub-graph executions when there is no matched states or cycles that contain all events; checking in the old ConflictTracker for testing.

20 months agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Wed, 25 Mar 2020 22:43:55 +0000 (15:43 -0700)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

20 months agoFixing bugs and cleaning up: making sure that the execution of the first trace has...
rtrimana [Wed, 25 Mar 2020 22:43:13 +0000 (15:43 -0700)]
Fixing bugs and cleaning up: making sure that the execution of the first trace has fair-scheduling with appropriate state-matching.

20 months agoMaking analysis compatible with infra
Seyed Amir Hossein Aqajari [Tue, 24 Mar 2020 22:51:11 +0000 (15:51 -0700)]
Making analysis compatible with infra

20 months agoMaking analysis compatible with new infrastructure
Seyed Amir Hossein Aqajari [Tue, 24 Mar 2020 22:50:03 +0000 (15:50 -0700)]
Making analysis compatible with new infrastructure

20 months agoCleaning up: Removing the full-blown graph traversal.
rtrimana [Mon, 23 Mar 2020 21:56:29 +0000 (14:56 -0700)]
Cleaning up: Removing the full-blown graph traversal.

20 months agoCleaning up, fixing bugs---commented out full-blown graph traversal code.
rtrimana [Mon, 23 Mar 2020 21:41:04 +0000 (14:41 -0700)]
Cleaning up, fixing bugs---commented out full-blown graph traversal code.

20 months agoRefactoring; Finding cycles without traversing the entire state graph.
rtrimana [Sat, 21 Mar 2020 04:34:59 +0000 (21:34 -0700)]
Refactoring; Finding cycles without traversing the entire state graph.

20 months agoFixing bugs: moving VOD-graph building into the CGAdvanced method to have the most...
rtrimana [Fri, 20 Mar 2020 21:11:09 +0000 (14:11 -0700)]
Fixing bugs: moving VOD-graph building into the CGAdvanced method to have the most up-to-date values.

20 months agoAdding graph traversal to find cycles; adding debug mode for ConflictTracker.
rtrimana [Thu, 19 Mar 2020 18:14:58 +0000 (11:14 -0700)]
Adding graph traversal to find cycles; adding debug mode for ConflictTracker.

20 months agoSome fixes for the DPOR state-reducer.
rtrimana [Mon, 16 Mar 2020 20:44:02 +0000 (13:44 -0700)]
Some fixes for the DPOR state-reducer.

20 months agoFixing a bug: merging the analysis part for locationMode w.r.t manual interaction...
rtrimana [Mon, 2 Mar 2020 22:12:31 +0000 (14:12 -0800)]
Fixing a bug: merging the analysis part for locationMode w.r.t manual interaction flag.

20 months agoFix for a bug in finding the right integer values in the stack frame: need to find...
rtrimana [Fri, 28 Feb 2020 21:36:27 +0000 (13:36 -0800)]
Fix for a bug in finding the right integer values in the stack frame: need to find a value that's not 0 in the frame (previously we only look at offset 0 or 1 because of adapting the function getValue() from a listener for Java code).

20 months agoAdding attributes for dimmers.
rtrimana [Fri, 28 Feb 2020 19:31:36 +0000 (11:31 -0800)]
Adding attributes for dimmers.

21 months agoCode to print graph to output so that dot can be used to generate pdf of graph.
Brian Demsky [Wed, 26 Feb 2020 21:19:26 +0000 (13:19 -0800)]
Code to print graph to output so that dot can be used to generate pdf of graph.

21 months agoAdding manual transactions to the conflict tracker
Seyed Amir Hossein Aqajari [Wed, 19 Feb 2020 19:21:38 +0000 (11:21 -0800)]
Adding manual transactions to the conflict tracker

21 months agoSlight changes for safeguard.
rtrimana [Sat, 15 Feb 2020 00:11:23 +0000 (16:11 -0800)]
Slight changes for safeguard.

21 months agoFixing an out of bound bug.
rtrimana [Fri, 14 Feb 2020 18:32:06 +0000 (10:32 -0800)]
Fixing an out of bound bug.

21 months agoJPF ready to run with old infrastructure
Seyed Amir Hossein Aqajari [Thu, 13 Feb 2020 21:39:36 +0000 (13:39 -0800)]
JPF ready to run with old infrastructure

21 months agoAdding a prevChoiceValue class property to store the previous choice to update the...
rtrimana [Mon, 10 Feb 2020 21:38:03 +0000 (13:38 -0800)]
Adding a prevChoiceValue class property to store the previous choice to update the VOD graph correctly.

21 months agoAttempting state-based DPOR implementation from the SPIN paper.
rtrimana [Fri, 7 Feb 2020 23:08:59 +0000 (15:08 -0800)]
Attempting state-based DPOR implementation from the SPIN paper.

21 months agoAdding the first implementation of visible operation dependency graph for stateful...
rtrimana [Thu, 30 Jan 2020 20:08:01 +0000 (12:08 -0800)]
Adding the first implementation of visible operation dependency graph for stateful DPOR: need to do more test to make sure that it's really working.

23 months agoMake updates and not edges have manual property
Brian Demsky [Tue, 17 Dec 2019 06:57:19 +0000 (22:57 -0800)]
Make updates and not edges have manual property

23 months agoClean up comments
Brian Demsky [Tue, 17 Dec 2019 06:41:16 +0000 (22:41 -0800)]
Clean up comments

23 months agoRewrite of Conflict Tracker
Brian Demsky [Tue, 17 Dec 2019 06:35:45 +0000 (22:35 -0800)]
Rewrite of Conflict Tracker

23 months agoA change in updateTheOutSet in conflict tracker analysis
amiraj [Tue, 17 Dec 2019 01:03:33 +0000 (17:03 -0800)]
A change in updateTheOutSet in conflict tracker analysis

23 months agoA change in propagate method.
amiraj [Thu, 12 Dec 2019 22:30:53 +0000 (14:30 -0800)]
A change in propagate method.

23 months agoFixing a bug in Conflict Tracker + Make propagate method much simpler
amiraj [Thu, 12 Dec 2019 20:34:21 +0000 (12:34 -0800)]
Fixing a bug in Conflict Tracker + Make propagate method much simpler

23 months agoMake a change in ConflictTracker analysis
amiraj [Wed, 11 Dec 2019 21:21:41 +0000 (13:21 -0800)]
Make a change in ConflictTracker analysis

23 months agoCompacting the methods
Seyed Amir Hossein Aqajari [Sat, 7 Dec 2019 00:25:17 +0000 (16:25 -0800)]
Compacting the methods

23 months agoA change in propagate the change method
Seyed Amir Hossein Aqajari [Fri, 6 Dec 2019 22:46:04 +0000 (14:46 -0800)]
A change in propagate the change method

23 months agoMake the analysis more efficient
Seyed Amir Hossein Aqajari [Fri, 6 Dec 2019 20:46:02 +0000 (12:46 -0800)]
Make the analysis more efficient

23 months agoFixing a small bug in Conflict Tracker
Seyed Amir Hossein Aqajari [Fri, 6 Dec 2019 20:36:29 +0000 (12:36 -0800)]
Fixing a small bug in Conflict Tracker

23 months agoFixing bugs in Conflict Tracker
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 23:40:05 +0000 (15:40 -0800)]
Fixing bugs in Conflict Tracker

23 months agoFixing a bug
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 22:48:15 +0000 (14:48 -0800)]
Fixing a bug

23 months agoFixing a bug in checkForConflict method in Conflict Tracker analysis!
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 22:45:43 +0000 (14:45 -0800)]
Fixing a bug in checkForConflict method in Conflict Tracker analysis!

23 months agoFixing a bug in manual_write-non_conflict + setSet conflicts
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 22:15:39 +0000 (14:15 -0800)]
Fixing a bug in manual_write-non_conflict + setSet conflicts

23 months agoFixing a bug in Conflict Tracker analysis
Seyed Amir Hossein Aqajari [Thu, 5 Dec 2019 19:47:54 +0000 (11:47 -0800)]
Fixing a bug in Conflict Tracker analysis

23 months agoMerge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core
rtrimana [Wed, 4 Dec 2019 21:20:19 +0000 (13:20 -0800)]
Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core