From 8926c7913a6512e64cb598344fcf1e3fc3b2bb4a Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Fri, 9 Aug 2024 15:55:01 +0200 Subject: [PATCH] Location-based ws #316 --- .../arrays/allocations-fields/report.json | 2 +- .../arrays/allocations/report.json | 2 +- .../imp-testcases/arrays/monolith/report.json | 2 +- .../imp-testcases/dataflow/ae/report.json | 2 +- .../imp-testcases/dataflow/cp/report.json | 2 +- .../dataflow/liveness/report.json | 2 +- .../imp-testcases/dataflow/rd/report.json | 2 +- .../descending/maxglb/report.json | 2 +- .../descending/widening/report.json | 2 +- .../imp-testcases/heap/pp-field/report.json | 2 +- .../imp-testcases/heap/pp/report.json | 2 +- .../imp-testcases/heap/types/report.json | 2 +- .../context-helper-full/report.json | 2 +- .../context-helper-last/report.json | 2 +- .../context-pp-arrayop/report.json | 2 +- .../context-pp-twoarrays/report.json | 2 +- .../interprocedural/context/report.json | 2 +- .../factorial/full/report.json | 2 +- .../factorial/insensitive/report.json | 2 +- .../factorial/kdepth/report.json | 2 +- .../factorial/last/report.json | 2 +- .../factorialInterleaved/full/report.json | 2 +- .../insensitive/report.json | 2 +- .../factorialInterleaved/kdepth/report.json | 2 +- .../factorialInterleaved/last/report.json | 2 +- .../factorialLoop/full/report.json | 2 +- .../factorialLoop/insensitive/report.json | 2 +- .../factorialLoop/kdepth/report.json | 2 +- .../factorialLoop/last/report.json | 2 +- .../fibonacci/full/report.json | 2 +- .../fibonacci/insensitive/report.json | 2 +- .../fibonacci/kdepth/report.json | 2 +- .../fibonacci/last/report.json | 2 +- .../infiniteRecursion1/full/report.json | 2 +- .../insensitive/report.json | 2 +- .../infiniteRecursion1/kdepth/report.json | 2 +- .../infiniteRecursion1/last/report.json | 2 +- .../infiniteRecursion2/full/report.json | 2 +- .../insensitive/report.json | 2 +- .../infiniteRecursion2/kdepth/report.json | 2 +- .../infiniteRecursion2/last/report.json | 2 +- .../interprocedural/modular-cha/report.json | 2 +- .../interprocedural/modular-rta/report.json | 2 +- .../nestedRecursions/full/report.json | 2 +- .../nestedRecursions/insensitive/report.json | 2 +- .../nestedRecursions/kdepth/report.json | 2 +- .../nestedRecursions/last/report.json | 2 +- .../twoRecursions/full/report.json | 2 +- .../twoRecursions/insensitive/report.json | 2 +- .../twoRecursions/kdepth/report.json | 2 +- .../twoRecursions/last/report.json | 2 +- .../unreachableBaseCase/full/report.json | 2 +- .../insensitive/report.json | 2 +- .../unreachableBaseCase/kdepth/report.json | 2 +- .../unreachableBaseCase/last/report.json | 2 +- .../confidentiality/report.json | 2 +- .../non-interference/integrity/report.json | 2 +- .../non-interference/interproc/report.json | 2 +- .../numeric/int-const/report.json | 2 +- .../numeric/interval-set/report.json | 8 +- .../untyped_tutorial.sat(tutorial__this).json | 2 +- .../numeric/interval/report.json | 2 +- .../imp-testcases/numeric/parity/report.json | 2 +- .../numeric/pentagons/report.json | 2 +- .../imp-testcases/numeric/sign/report.json | 2 +- .../imp-testcases/stability/report.json | 2 +- .../imp-testcases/string/bricks/report.json | 2 +- .../string/char-inclusion/report.json | 2 +- .../imp-testcases/string/fsa/report.json | 2 +- .../imp-testcases/string/prefix/report.json | 2 +- .../string/subs-domain-constants/report.json | 2 +- .../string/subs-domain/report.json | 2 +- .../imp-testcases/string/suffix/report.json | 2 +- .../imp-testcases/string/tarsis/report.json | 2 +- .../imp-testcases/syntactic/report.json | 2 +- .../imp-testcases/taint/2val/report.json | 2 +- .../imp-testcases/taint/3val/report.json | 2 +- .../imp-testcases/traces/report.json | 2 +- .../imp-testcases/type-inference/report.json | 2 +- .../visualization/dot/report.json | 2 +- .../visualization/graphml-sub/report.json | 2 +- .../visualization/graphml/report.json | 2 +- .../visualization/html-inputs/report.json | 2 +- .../visualization/html-sub/report.json | 2 +- .../visualization/html/report.json | 2 +- .../visualization/inputs/report.json | 2 +- .../BackwardModularWorstCaseAnalysis.java | 4 +- .../ModularWorstCaseAnalysis.java | 5 +- .../context/ContextBasedAnalysis.java | 3 +- .../context/recursion/BaseCasesFinder.java | 3 - .../context/recursion/RecursionSolver.java | 3 - .../EqualityContractVerificationTest.java | 2 + .../main/java/it/unive/lisa/LiSARunner.java | 3 - .../BackwardOptimizedAnalyzedCFG.java | 2 - .../lisa/analysis/OptimizedAnalyzedCFG.java | 4 +- .../lisa/conf/FixpointConfiguration.java | 8 ++ .../it/unive/lisa/conf/LiSAConfiguration.java | 6 +- .../InterproceduralAnalysis.java | 12 +-- .../workset/OrderBasedWorkingSet.java | 98 +++++++++++++++++++ .../lisa/TestInterproceduralAnalysis.java | 3 - 100 files changed, 209 insertions(+), 125 deletions(-) create mode 100644 lisa/lisa-sdk/src/main/java/it/unive/lisa/util/collections/workset/OrderBasedWorkingSet.java diff --git a/lisa/lisa-analyses/imp-testcases/arrays/allocations-fields/report.json b/lisa/lisa-analyses/imp-testcases/arrays/allocations-fields/report.json index 28468fdbc..9efedd483 100644 --- a/lisa/lisa-analyses/imp-testcases/arrays/allocations-fields/report.json +++ b/lisa/lisa-analyses/imp-testcases/arrays/allocations-fields/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/arrays/allocations/report.json b/lisa/lisa-analyses/imp-testcases/arrays/allocations/report.json index e40fb17c2..be0fda458 100644 --- a/lisa/lisa-analyses/imp-testcases/arrays/allocations/report.json +++ b/lisa/lisa-analyses/imp-testcases/arrays/allocations/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/arrays/monolith/report.json b/lisa/lisa-analyses/imp-testcases/arrays/monolith/report.json index cf3996f0e..2adf43ecd 100644 --- a/lisa/lisa-analyses/imp-testcases/arrays/monolith/report.json +++ b/lisa/lisa-analyses/imp-testcases/arrays/monolith/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/dataflow/ae/report.json b/lisa/lisa-analyses/imp-testcases/dataflow/ae/report.json index 477399150..856e8c89a 100644 --- a/lisa/lisa-analyses/imp-testcases/dataflow/ae/report.json +++ b/lisa/lisa-analyses/imp-testcases/dataflow/ae/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/dataflow/cp/report.json b/lisa/lisa-analyses/imp-testcases/dataflow/cp/report.json index b2c8fe901..e0c4340a0 100644 --- a/lisa/lisa-analyses/imp-testcases/dataflow/cp/report.json +++ b/lisa/lisa-analyses/imp-testcases/dataflow/cp/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/dataflow/liveness/report.json b/lisa/lisa-analyses/imp-testcases/dataflow/liveness/report.json index 0b880fcea..4c9d92d8c 100644 --- a/lisa/lisa-analyses/imp-testcases/dataflow/liveness/report.json +++ b/lisa/lisa-analyses/imp-testcases/dataflow/liveness/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/dataflow/rd/report.json b/lisa/lisa-analyses/imp-testcases/dataflow/rd/report.json index 1c09d1a60..60003e724 100644 --- a/lisa/lisa-analyses/imp-testcases/dataflow/rd/report.json +++ b/lisa/lisa-analyses/imp-testcases/dataflow/rd/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/descending/maxglb/report.json b/lisa/lisa-analyses/imp-testcases/descending/maxglb/report.json index 6be02d1ba..8af18c92f 100644 --- a/lisa/lisa-analyses/imp-testcases/descending/maxglb/report.json +++ b/lisa/lisa-analyses/imp-testcases/descending/maxglb/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "GLB", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/descending/widening/report.json b/lisa/lisa-analyses/imp-testcases/descending/widening/report.json index dee57b530..9a4b6c8c8 100644 --- a/lisa/lisa-analyses/imp-testcases/descending/widening/report.json +++ b/lisa/lisa-analyses/imp-testcases/descending/widening/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NARROWING", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/heap/pp-field/report.json b/lisa/lisa-analyses/imp-testcases/heap/pp-field/report.json index 84d017ae5..0b54e54cf 100644 --- a/lisa/lisa-analyses/imp-testcases/heap/pp-field/report.json +++ b/lisa/lisa-analyses/imp-testcases/heap/pp-field/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/heap/pp/report.json b/lisa/lisa-analyses/imp-testcases/heap/pp/report.json index 6cb072e9b..cf3904928 100644 --- a/lisa/lisa-analyses/imp-testcases/heap/pp/report.json +++ b/lisa/lisa-analyses/imp-testcases/heap/pp/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/heap/types/report.json b/lisa/lisa-analyses/imp-testcases/heap/types/report.json index ccfd75435..732022d60 100644 --- a/lisa/lisa-analyses/imp-testcases/heap/types/report.json +++ b/lisa/lisa-analyses/imp-testcases/heap/types/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/context-helper-full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/context-helper-full/report.json index 2d66b6392..f97919960 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/context-helper-full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/context-helper-full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/context-helper-last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/context-helper-last/report.json index 5192e08b7..ec701078d 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/context-helper-last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/context-helper-last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/context-pp-arrayop/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/context-pp-arrayop/report.json index 57dbdc569..b1157ed91 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/context-pp-arrayop/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/context-pp-arrayop/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/context-pp-twoarrays/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/context-pp-twoarrays/report.json index c2a718ff6..997e7333d 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/context-pp-twoarrays/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/context-pp-twoarrays/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/context/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/context/report.json index 7deb0e08e..7dfa3442b 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/context/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/context/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/full/report.json index 1c0571223..baae943d0 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/insensitive/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/insensitive/report.json index f74bae046..9c5ed516c 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/insensitive/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/insensitive/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/kdepth/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/kdepth/report.json index 4e05381b0..6655878a0 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/kdepth/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/kdepth/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/last/report.json index 30378cf92..d159fdca5 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorial/last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/full/report.json index 39114b42a..ab7e53d47 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/insensitive/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/insensitive/report.json index bffb3dc41..ed2b562ea 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/insensitive/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/insensitive/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/kdepth/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/kdepth/report.json index 015bcf81f..c717a6cc6 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/kdepth/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/kdepth/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/last/report.json index 281f1fac5..64bdfbc40 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialInterleaved/last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/full/report.json index 211b23a89..892b97565 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/insensitive/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/insensitive/report.json index d73a7931b..d9d875608 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/insensitive/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/insensitive/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/kdepth/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/kdepth/report.json index e6805eaba..b65ed23ef 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/kdepth/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/kdepth/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/last/report.json index 809c3e77e..f999649b3 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/factorialLoop/last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/full/report.json index 1146d609b..3e47f78a8 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/insensitive/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/insensitive/report.json index 8c2a88bdf..b9ca9b3c1 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/insensitive/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/insensitive/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/kdepth/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/kdepth/report.json index 9b7af5e9c..e35bceccc 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/kdepth/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/kdepth/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/last/report.json index 63aa152c5..baf64c71d 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/fibonacci/last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/full/report.json index f134937ad..3d1fe89f6 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/insensitive/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/insensitive/report.json index 03ad433b0..5a3e0d052 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/insensitive/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/insensitive/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/kdepth/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/kdepth/report.json index 5cb251a6a..be5fb43f3 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/kdepth/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/kdepth/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/last/report.json index 3d113950c..17fe8bdc6 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion1/last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/full/report.json index 36b6f38a8..90dd00221 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/insensitive/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/insensitive/report.json index f52b8e9ae..a37a1f928 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/insensitive/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/insensitive/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/kdepth/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/kdepth/report.json index 29196f5cb..17c0ed9b7 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/kdepth/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/kdepth/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/last/report.json index ba5bd3b1a..21f498421 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/infiniteRecursion2/last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/modular-cha/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/modular-cha/report.json index b1480801d..3fbe10227 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/modular-cha/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/modular-cha/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/modular-rta/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/modular-rta/report.json index 822cf6116..ff5388aa7 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/modular-rta/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/modular-rta/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/full/report.json index 7180cce00..319d1f044 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/insensitive/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/insensitive/report.json index 5e7dc140b..5851dd63e 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/insensitive/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/insensitive/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/kdepth/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/kdepth/report.json index bc59e7346..9be710180 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/kdepth/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/kdepth/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/last/report.json index 63818b3ae..94514af45 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/nestedRecursions/last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/full/report.json index 7b9a7b424..e813cecae 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/insensitive/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/insensitive/report.json index 890fa4779..46bbe2a36 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/insensitive/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/insensitive/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/kdepth/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/kdepth/report.json index d7fd97fc8..b7244d8ff 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/kdepth/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/kdepth/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/last/report.json index c590e7086..3d452cc71 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/twoRecursions/last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/full/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/full/report.json index 68fcde3e0..b178319ad 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/full/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/full/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/insensitive/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/insensitive/report.json index 12123c8a2..d936de3e0 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/insensitive/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/insensitive/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/kdepth/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/kdepth/report.json index 054db8d08..e5a8d75ec 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/kdepth/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/kdepth/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/last/report.json b/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/last/report.json index 5acb86ab2..ff49779d2 100644 --- a/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/last/report.json +++ b/lisa/lisa-analyses/imp-testcases/interprocedural/unreachableBaseCase/last/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/non-interference/confidentiality/report.json b/lisa/lisa-analyses/imp-testcases/non-interference/confidentiality/report.json index 49e367fba..6cf575a61 100644 --- a/lisa/lisa-analyses/imp-testcases/non-interference/confidentiality/report.json +++ b/lisa/lisa-analyses/imp-testcases/non-interference/confidentiality/report.json @@ -40,7 +40,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "set", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/non-interference/integrity/report.json b/lisa/lisa-analyses/imp-testcases/non-interference/integrity/report.json index 98362d8f3..303bd7a85 100644 --- a/lisa/lisa-analyses/imp-testcases/non-interference/integrity/report.json +++ b/lisa/lisa-analyses/imp-testcases/non-interference/integrity/report.json @@ -40,7 +40,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "set", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/non-interference/interproc/report.json b/lisa/lisa-analyses/imp-testcases/non-interference/interproc/report.json index 16a3bd2f0..79149aabf 100644 --- a/lisa/lisa-analyses/imp-testcases/non-interference/interproc/report.json +++ b/lisa/lisa-analyses/imp-testcases/non-interference/interproc/report.json @@ -26,7 +26,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "set", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/numeric/int-const/report.json b/lisa/lisa-analyses/imp-testcases/numeric/int-const/report.json index a2b6cd7d1..49c923d6a 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/int-const/report.json +++ b/lisa/lisa-analyses/imp-testcases/numeric/int-const/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/numeric/interval-set/report.json b/lisa/lisa-analyses/imp-testcases/numeric/interval-set/report.json index 4d8f867d6..24a478007 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/interval-set/report.json +++ b/lisa/lisa-analyses/imp-testcases/numeric/interval-set/report.json @@ -3,14 +3,14 @@ "files" : [ "report.json", "untyped_tutorial.constants(tutorial__this).json", "untyped_tutorial.div(tutorial__this,_untyped_i,_untyped_j).json", "untyped_tutorial.doublewhile(tutorial__this,_untyped_t).json", "untyped_tutorial.gcd(tutorial__this,_untyped_a,_untyped_b).json", "untyped_tutorial.glb(tutorial__this,_untyped_x,_untyped_y).json", "untyped_tutorial.intv_dec(tutorial__this).json", "untyped_tutorial.sat(tutorial__this).json", "untyped_tutorial.sat(tutorial__this,_untyped_x,_untyped_y).json", "untyped_tutorial.sat2(tutorial__this).json", "untyped_tutorial.sign_parity_example(tutorial__this).json", "untyped_tutorial.ub_example(tutorial__this,_untyped_y,_untyped_z).json" ], "info" : { "cfgs" : "11", - "duration" : "334ms", - "end" : "2023-12-05T12:59:31.404+01:00", + "duration" : "906ms", + "end" : "2024-08-09T15:50:22.551+02:00", "expressions" : "153", "files" : "11", "globals" : "0", "members" : "11", "programs" : "1", - "start" : "2023-12-05T12:59:31.070+01:00", + "start" : "2024-08-09T15:50:21.645+02:00", "statements" : "62", "units" : "1", "version" : "0.1b8", @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "GLB", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/numeric/interval-set/untyped_tutorial.sat(tutorial__this).json b/lisa/lisa-analyses/imp-testcases/numeric/interval-set/untyped_tutorial.sat(tutorial__this).json index 1caef9351..c17502b62 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/interval-set/untyped_tutorial.sat(tutorial__this).json +++ b/lisa/lisa-analyses/imp-testcases/numeric/interval-set/untyped_tutorial.sat(tutorial__this).json @@ -1 +1 @@ -{"name":"untyped tutorial::sat(tutorial* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = 0"},{"id":1,"text":"x"},{"id":2,"text":"0"},{"id":3,"subNodes":[4,5],"text":"<(x, 100)"},{"id":4,"text":"x"},{"id":5,"text":"100"},{"id":6,"subNodes":[7,8],"text":">(x, 50)"},{"id":7,"text":"x"},{"id":8,"text":"50"},{"id":9,"subNodes":[10,11],"text":"x = +(x, 10)"},{"id":10,"text":"x"},{"id":11,"subNodes":[12,13],"text":"+(x, 10)"},{"id":12,"text":"x"},{"id":13,"text":"10"},{"id":14,"subNodes":[15,16],"text":"x = +(x, 2)"},{"id":15,"text":"x"},{"id":16,"subNodes":[17,18],"text":"+(x, 2)"},{"id":17,"text":"x"},{"id":18,"text":"2"},{"id":19,"subNodes":[20],"text":"return x"},{"id":20,"text":"x"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"TrueEdge"},{"sourceId":3,"destId":19,"kind":"FalseEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":14,"kind":"FalseEdge"},{"sourceId":9,"destId":3,"kind":"SequentialEdge"},{"sourceId":14,"destId":3,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]"]}}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"this":["tutorial*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["x < 100"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[101, 109]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 52]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":4,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[101, 109]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 52]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":5,"description":{"expressions":["100"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[101, 109]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 52]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":6,"description":{"expressions":["x > 50"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 52]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 52]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":8,"description":{"expressions":["50"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 52]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":9,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[101, 102]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":10,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[51, 52]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":11,"description":{"expressions":["x + 10"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[51, 52]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[51, 52]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":13,"description":{"expressions":["10"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[51, 52]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":14,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[10, 10]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 20]","[22, 52]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 50]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":16,"description":{"expressions":["x + 2"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 50]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":17,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 50]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":18,"description":{"expressions":["2"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 10]","[12, 12]","[14, 14]","[16, 16]","[18, 18]","[2, 2]","[20, 50]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":19,"description":{"expressions":["ret_value@sat"],"state":{"heap":"monolith","type":{"ret_value@sat":["int32"],"this":["tutorial*"],"x":["int32"]},"value":{"ret_value@sat":["[101, 109]"],"x":["[101, 109]"]}}}},{"nodeId":20,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[101, 109]"]}}}}]} \ No newline at end of file +{"name":"untyped tutorial::sat(tutorial* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = 0"},{"id":1,"text":"x"},{"id":2,"text":"0"},{"id":3,"subNodes":[4,5],"text":"<(x, 100)"},{"id":4,"text":"x"},{"id":5,"text":"100"},{"id":6,"subNodes":[7,8],"text":">(x, 50)"},{"id":7,"text":"x"},{"id":8,"text":"50"},{"id":9,"subNodes":[10,11],"text":"x = +(x, 10)"},{"id":10,"text":"x"},{"id":11,"subNodes":[12,13],"text":"+(x, 10)"},{"id":12,"text":"x"},{"id":13,"text":"10"},{"id":14,"subNodes":[15,16],"text":"x = +(x, 2)"},{"id":15,"text":"x"},{"id":16,"subNodes":[17,18],"text":"+(x, 2)"},{"id":17,"text":"x"},{"id":18,"text":"2"},{"id":19,"subNodes":[20],"text":"return x"},{"id":20,"text":"x"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"TrueEdge"},{"sourceId":3,"destId":19,"kind":"FalseEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":14,"kind":"FalseEdge"},{"sourceId":9,"destId":3,"kind":"SequentialEdge"},{"sourceId":14,"destId":3,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]"]}}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"this":["tutorial*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["x < 100"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 52]","[101, 109]","[2, 2]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":4,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 52]","[101, 109]","[2, 2]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":5,"description":{"expressions":["100"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 52]","[101, 109]","[2, 2]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":6,"description":{"expressions":["x > 50"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 52]","[2, 2]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 52]","[2, 2]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":8,"description":{"expressions":["50"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 52]","[2, 2]","[4, 4]","[6, 6]","[61, 62]","[71, 72]","[8, 8]","[81, 82]","[91, 92]"]}}}},{"nodeId":9,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[101, 102]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":10,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[51, 52]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":11,"description":{"expressions":["x + 10"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[51, 52]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[51, 52]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":13,"description":{"expressions":["10"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[51, 52]","[61, 62]","[71, 72]","[81, 82]","[91, 92]"]}}}},{"nodeId":14,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[10, 10]","[12, 52]","[2, 2]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 50]","[2, 2]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":16,"description":{"expressions":["x + 2"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 50]","[2, 2]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":17,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 50]","[2, 2]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":18,"description":{"expressions":["2"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[0, 0]","[10, 50]","[2, 2]","[4, 4]","[6, 6]","[8, 8]"]}}}},{"nodeId":19,"description":{"expressions":["ret_value@sat"],"state":{"heap":"monolith","type":{"ret_value@sat":["int32"],"this":["tutorial*"],"x":["int32"]},"value":{"ret_value@sat":["[101, 109]"],"x":["[101, 109]"]}}}},{"nodeId":20,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["tutorial*"],"x":["int32"]},"value":{"x":["[101, 109]"]}}}}]} \ No newline at end of file diff --git a/lisa/lisa-analyses/imp-testcases/numeric/interval/report.json b/lisa/lisa-analyses/imp-testcases/numeric/interval/report.json index 65da18dea..486082a61 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/interval/report.json +++ b/lisa/lisa-analyses/imp-testcases/numeric/interval/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/numeric/parity/report.json b/lisa/lisa-analyses/imp-testcases/numeric/parity/report.json index 69fa2ebdb..c9e6270bb 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/parity/report.json +++ b/lisa/lisa-analyses/imp-testcases/numeric/parity/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json index 785518ce3..2686530c9 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json +++ b/lisa/lisa-analyses/imp-testcases/numeric/pentagons/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/numeric/sign/report.json b/lisa/lisa-analyses/imp-testcases/numeric/sign/report.json index cfac9178b..45b2be24c 100644 --- a/lisa/lisa-analyses/imp-testcases/numeric/sign/report.json +++ b/lisa/lisa-analyses/imp-testcases/numeric/sign/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/stability/report.json b/lisa/lisa-analyses/imp-testcases/stability/report.json index 6ef326221..0b974ff71 100644 --- a/lisa/lisa-analyses/imp-testcases/stability/report.json +++ b/lisa/lisa-analyses/imp-testcases/stability/report.json @@ -26,7 +26,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/string/bricks/report.json b/lisa/lisa-analyses/imp-testcases/string/bricks/report.json index 601a45b88..454b8bed5 100644 --- a/lisa/lisa-analyses/imp-testcases/string/bricks/report.json +++ b/lisa/lisa-analyses/imp-testcases/string/bricks/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/string/char-inclusion/report.json b/lisa/lisa-analyses/imp-testcases/string/char-inclusion/report.json index fa08e18fc..c30c3fb29 100644 --- a/lisa/lisa-analyses/imp-testcases/string/char-inclusion/report.json +++ b/lisa/lisa-analyses/imp-testcases/string/char-inclusion/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/string/fsa/report.json b/lisa/lisa-analyses/imp-testcases/string/fsa/report.json index 9a3c094d1..6e32a4219 100644 --- a/lisa/lisa-analyses/imp-testcases/string/fsa/report.json +++ b/lisa/lisa-analyses/imp-testcases/string/fsa/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/string/prefix/report.json b/lisa/lisa-analyses/imp-testcases/string/prefix/report.json index 22de04bde..42a847fee 100644 --- a/lisa/lisa-analyses/imp-testcases/string/prefix/report.json +++ b/lisa/lisa-analyses/imp-testcases/string/prefix/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json b/lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json index 0626aad41..f8bd577a0 100644 --- a/lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json +++ b/lisa/lisa-analyses/imp-testcases/string/subs-domain-constants/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json b/lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json index b1186d127..f8d8d8e34 100644 --- a/lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json +++ b/lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/string/suffix/report.json b/lisa/lisa-analyses/imp-testcases/string/suffix/report.json index 026f56162..daee813a2 100644 --- a/lisa/lisa-analyses/imp-testcases/string/suffix/report.json +++ b/lisa/lisa-analyses/imp-testcases/string/suffix/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/string/tarsis/report.json b/lisa/lisa-analyses/imp-testcases/string/tarsis/report.json index 3ec69311e..2ed098926 100644 --- a/lisa/lisa-analyses/imp-testcases/string/tarsis/report.json +++ b/lisa/lisa-analyses/imp-testcases/string/tarsis/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/syntactic/report.json b/lisa/lisa-analyses/imp-testcases/syntactic/report.json index cb053b8c7..32d092190 100644 --- a/lisa/lisa-analyses/imp-testcases/syntactic/report.json +++ b/lisa/lisa-analyses/imp-testcases/syntactic/report.json @@ -38,7 +38,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/taint/2val/report.json b/lisa/lisa-analyses/imp-testcases/taint/2val/report.json index 847e197bd..85d97b27e 100644 --- a/lisa/lisa-analyses/imp-testcases/taint/2val/report.json +++ b/lisa/lisa-analyses/imp-testcases/taint/2val/report.json @@ -84,7 +84,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "set", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/taint/3val/report.json b/lisa/lisa-analyses/imp-testcases/taint/3val/report.json index 64e000d25..a73f9603a 100644 --- a/lisa/lisa-analyses/imp-testcases/taint/3val/report.json +++ b/lisa/lisa-analyses/imp-testcases/taint/3val/report.json @@ -84,7 +84,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "set", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/traces/report.json b/lisa/lisa-analyses/imp-testcases/traces/report.json index 2420b8558..866fa55a9 100644 --- a/lisa/lisa-analyses/imp-testcases/traces/report.json +++ b/lisa/lisa-analyses/imp-testcases/traces/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/type-inference/report.json b/lisa/lisa-analyses/imp-testcases/type-inference/report.json index d1e0c8048..53aafd5b8 100644 --- a/lisa/lisa-analyses/imp-testcases/type-inference/report.json +++ b/lisa/lisa-analyses/imp-testcases/type-inference/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/visualization/dot/report.json b/lisa/lisa-analyses/imp-testcases/visualization/dot/report.json index 9827e5f6c..71fb5aba8 100644 --- a/lisa/lisa-analyses/imp-testcases/visualization/dot/report.json +++ b/lisa/lisa-analyses/imp-testcases/visualization/dot/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "DOT", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/visualization/graphml-sub/report.json b/lisa/lisa-analyses/imp-testcases/visualization/graphml-sub/report.json index d8f49beb6..bf2edf2e4 100644 --- a/lisa/lisa-analyses/imp-testcases/visualization/graphml-sub/report.json +++ b/lisa/lisa-analyses/imp-testcases/visualization/graphml-sub/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "GRAPHML_WITH_SUBNODES", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/visualization/graphml/report.json b/lisa/lisa-analyses/imp-testcases/visualization/graphml/report.json index 8fb854bf9..0323fe014 100644 --- a/lisa/lisa-analyses/imp-testcases/visualization/graphml/report.json +++ b/lisa/lisa-analyses/imp-testcases/visualization/graphml/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "GRAPHML", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/visualization/html-inputs/report.json b/lisa/lisa-analyses/imp-testcases/visualization/html-inputs/report.json index a893108d3..85cee3ab5 100644 --- a/lisa/lisa-analyses/imp-testcases/visualization/html-inputs/report.json +++ b/lisa/lisa-analyses/imp-testcases/visualization/html-inputs/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "HTML", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/visualization/html-sub/report.json b/lisa/lisa-analyses/imp-testcases/visualization/html-sub/report.json index f0c3b1881..6e8163744 100644 --- a/lisa/lisa-analyses/imp-testcases/visualization/html-sub/report.json +++ b/lisa/lisa-analyses/imp-testcases/visualization/html-sub/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "HTML_WITH_SUBNODES", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/visualization/html/report.json b/lisa/lisa-analyses/imp-testcases/visualization/html/report.json index 0dfcfae1b..283367cee 100644 --- a/lisa/lisa-analyses/imp-testcases/visualization/html/report.json +++ b/lisa/lisa-analyses/imp-testcases/visualization/html/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "HTML", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/imp-testcases/visualization/inputs/report.json b/lisa/lisa-analyses/imp-testcases/visualization/inputs/report.json index 600d3c889..5b6c7717a 100644 --- a/lisa/lisa-analyses/imp-testcases/visualization/inputs/report.json +++ b/lisa/lisa-analyses/imp-testcases/visualization/inputs/report.json @@ -20,7 +20,7 @@ "analysisGraphs" : "NONE", "descendingPhaseType" : "NONE", "dumpForcesUnwinding" : "false", - "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", + "fixpointWorkingSet" : "OrderBasedWorkingSet", "glbThreshold" : "5", "hotspots" : "unset", "jsonOutput" : "true", diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/BackwardModularWorstCaseAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/BackwardModularWorstCaseAnalysis.java index 7d73b8cd0..9af9ed16b 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/BackwardModularWorstCaseAnalysis.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/BackwardModularWorstCaseAnalysis.java @@ -14,7 +14,6 @@ import it.unive.lisa.logging.IterationLogger; import it.unive.lisa.program.Application; import it.unive.lisa.program.cfg.CFG; -import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.program.cfg.statement.call.CFGCall; import it.unive.lisa.program.cfg.statement.call.Call; import it.unive.lisa.program.cfg.statement.call.OpenCall; @@ -68,7 +67,6 @@ public boolean needsCallGraph() { @Override public void fixpoint( AnalysisState entryState, - Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException { if (conf.optimize) @@ -99,7 +97,7 @@ public void fixpoint( results.putResult(cfg, ID, cfg.backwardFixpoint( entryState, this, - WorkingSet.of(fixpointWorkingSet), + WorkingSet.of(conf.fixpointWorkingSet), conf, ID)); } catch (SemanticException e) { diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java index a51fad06e..3aba7b507 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java @@ -17,7 +17,6 @@ import it.unive.lisa.program.cfg.CodeLocation; import it.unive.lisa.program.cfg.Parameter; import it.unive.lisa.program.cfg.statement.Assignment; -import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.program.cfg.statement.VariableRef; import it.unive.lisa.program.cfg.statement.call.CFGCall; import it.unive.lisa.program.cfg.statement.call.Call; @@ -72,7 +71,6 @@ public boolean needsCallGraph() { @Override public void fixpoint( AnalysisState entryState, - Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException { // new fixpoint iteration: restart @@ -107,7 +105,8 @@ public void fixpoint( prepared = a.forwardSemantics(prepared, this, store); } - results.putResult(cfg, ID, cfg.fixpoint(prepared, this, WorkingSet.of(fixpointWorkingSet), conf, ID)); + results.putResult(cfg, ID, + cfg.fixpoint(prepared, this, WorkingSet.of(conf.fixpointWorkingSet), conf, ID)); } catch (SemanticException e) { throw new FixpointException("Error while creating the entrystate for " + cfg, e); } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java index facb3807d..ac8de3a0d 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java @@ -146,10 +146,9 @@ public void init( @Override public void fixpoint( AnalysisState entryState, - Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException { - this.workingSet = fixpointWorkingSet; + this.workingSet = conf.fixpointWorkingSet; this.conf = conf; // new fixpoint execution: reset this.results = null; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java index 77b769af8..cc16d7fbc 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java @@ -14,10 +14,8 @@ import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.fixpoints.CFGFixpoint.CompoundState; import it.unive.lisa.program.cfg.statement.Expression; -import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.program.cfg.statement.call.CFGCall; import it.unive.lisa.program.cfg.statement.call.Call; -import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; /** @@ -69,7 +67,6 @@ public void init( @Override public void fixpoint( AnalysisState entryState, - Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException { // we mark this as unsupported to make sure it never gets used as a root diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/RecursionSolver.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/RecursionSolver.java index 979f1a860..562a64a86 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/RecursionSolver.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/RecursionSolver.java @@ -17,13 +17,11 @@ import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.fixpoints.CFGFixpoint.CompoundState; import it.unive.lisa.program.cfg.statement.Expression; -import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.program.cfg.statement.call.CFGCall; import it.unive.lisa.program.cfg.statement.call.Call; import it.unive.lisa.symbolic.value.Identifier; import it.unive.lisa.symbolic.value.PushInv; import it.unive.lisa.util.StringUtilities; -import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; import java.util.Collection; import java.util.HashMap; @@ -94,7 +92,6 @@ public void init( @Override public void fixpoint( AnalysisState entryState, - Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException { // we mark this as unsupported to make sure it never gets used as a root diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/EqualityContractVerificationTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/EqualityContractVerificationTest.java index 39ac33400..80c526060 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/EqualityContractVerificationTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/EqualityContractVerificationTest.java @@ -96,6 +96,7 @@ import it.unive.lisa.util.collections.workset.DuplicateFreeLIFOWorkingSet; import it.unive.lisa.util.collections.workset.FIFOWorkingSet; import it.unive.lisa.util.collections.workset.LIFOWorkingSet; +import it.unive.lisa.util.collections.workset.OrderBasedWorkingSet; import it.unive.lisa.util.collections.workset.VisitOnceFIFOWorkingSet; import it.unive.lisa.util.collections.workset.VisitOnceLIFOWorkingSet; import it.unive.lisa.util.datastructures.automaton.Automaton; @@ -325,6 +326,7 @@ public void testCollections() { verify(VisitOnceLIFOWorkingSet.class); verify(DuplicateFreeFIFOWorkingSet.class); verify(DuplicateFreeLIFOWorkingSet.class); + verify(OrderBasedWorkingSet.class); } @Test diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java index 925372eea..309f9b6aa 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java @@ -30,7 +30,6 @@ import it.unive.lisa.type.ReferenceType; import it.unive.lisa.type.Type; import it.unive.lisa.type.TypeSystem; -import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; import it.unive.lisa.util.file.FileManager; import java.io.IOException; @@ -210,7 +209,6 @@ private boolean canAnalyze() { return true; } - @SuppressWarnings("unchecked") private void analyze( FixpointConfiguration fixconf) { A state = this.state.top(); @@ -219,7 +217,6 @@ private void analyze( try { interproc.fixpoint( new AnalysisState<>(state, new Skip(SyntheticLocation.INSTANCE)), - (Class>) conf.fixpointWorkingSet, fixconf); } catch (FixpointException e) { LOG.fatal("Exception during fixpoint computation", e); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/BackwardOptimizedAnalyzedCFG.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/BackwardOptimizedAnalyzedCFG.java index 413af5cdc..a329a9e84 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/BackwardOptimizedAnalyzedCFG.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/BackwardOptimizedAnalyzedCFG.java @@ -26,7 +26,6 @@ import it.unive.lisa.program.cfg.statement.call.UnresolvedCall; import it.unive.lisa.type.Type; import it.unive.lisa.util.collections.workset.FIFOWorkingSet; -import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.datastructures.graph.algorithms.BackwardFixpoint; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; import java.util.Collection; @@ -269,7 +268,6 @@ public void init( @Override public void fixpoint( AnalysisState exitState, - Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException { throw new UnsupportedOperationException(); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/OptimizedAnalyzedCFG.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/OptimizedAnalyzedCFG.java index 507c5e6a6..368f20c89 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/OptimizedAnalyzedCFG.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/OptimizedAnalyzedCFG.java @@ -25,7 +25,6 @@ import it.unive.lisa.program.cfg.statement.call.OpenCall; import it.unive.lisa.program.cfg.statement.call.UnresolvedCall; import it.unive.lisa.type.Type; -import it.unive.lisa.util.collections.workset.FIFOWorkingSet; import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.datastructures.graph.algorithms.Fixpoint; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; @@ -214,7 +213,7 @@ public void unwind( try { Map> res = fix.fixpoint( starting, - FIFOWorkingSet.mk(), + WorkingSet.of(conf.fixpointWorkingSet), asc, existing); expanded = new StatementStore<>(bottom); @@ -269,7 +268,6 @@ public void init( @Override public void fixpoint( AnalysisState entryState, - Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException { throw new UnsupportedOperationException(); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/FixpointConfiguration.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/FixpointConfiguration.java index ed69bbf9b..a0bbf1dc3 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/FixpointConfiguration.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/FixpointConfiguration.java @@ -2,6 +2,7 @@ import it.unive.lisa.conf.LiSAConfiguration.DescendingPhaseType; import it.unive.lisa.program.cfg.statement.Statement; +import it.unive.lisa.util.collections.workset.WorkingSet; import java.util.function.Predicate; /** @@ -11,6 +12,11 @@ */ public class FixpointConfiguration extends BaseConfiguration { + /** + * Holder of {@link LiSAConfiguration#fixpointWorkingSet}. + */ + public final Class> fixpointWorkingSet; + /** * Holder of {@link LiSAConfiguration#wideningThreshold}. */ @@ -51,8 +57,10 @@ public class FixpointConfiguration extends BaseConfiguration { * * @param parent the root configuration to draw data from. */ + @SuppressWarnings("unchecked") public FixpointConfiguration( LiSAConfiguration parent) { + this.fixpointWorkingSet = (Class>) parent.fixpointWorkingSet; this.wideningThreshold = parent.wideningThreshold; this.recursionWideningThreshold = parent.recursionWideningThreshold; this.glbThreshold = parent.glbThreshold; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/LiSAConfiguration.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/LiSAConfiguration.java index 84b8a1db3..87fbe479d 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/LiSAConfiguration.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/LiSAConfiguration.java @@ -16,7 +16,7 @@ import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.program.cfg.statement.call.OpenCall; import it.unive.lisa.util.collections.CollectionUtilities; -import it.unive.lisa.util.collections.workset.DuplicateFreeFIFOWorkingSet; +import it.unive.lisa.util.collections.workset.OrderBasedWorkingSet; import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.file.FileManager; import java.lang.reflect.Field; @@ -246,9 +246,9 @@ public static enum DescendingPhaseType { /** * The concrete class of {@link WorkingSet} to be used in fixpoints. - * Defaults to {@link DuplicateFreeFIFOWorkingSet}. + * Defaults to {@link OrderBasedWorkingSet}. */ - public Class fixpointWorkingSet = DuplicateFreeFIFOWorkingSet.class; + public Class fixpointWorkingSet = OrderBasedWorkingSet.class; /** * The {@link OpenCallPolicy} to be used for computing the result of diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/InterproceduralAnalysis.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/InterproceduralAnalysis.java index 2644fc240..8a59842cf 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/InterproceduralAnalysis.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/InterproceduralAnalysis.java @@ -15,7 +15,6 @@ import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.NativeCFG; import it.unive.lisa.program.cfg.statement.MetaVariableCreator; -import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.program.cfg.statement.call.CFGCall; import it.unive.lisa.program.cfg.statement.call.Call; import it.unive.lisa.program.cfg.statement.call.MultiCall; @@ -84,19 +83,16 @@ void init( * or one of its overloads. Results of individual cfgs are then available * through {@link #getAnalysisResultsOf(CFG)}. * - * @param entryState the entry state for the {@link CFG}s that are - * the entrypoints of the computation - * @param fixpointWorkingSet the concrete class of {@link WorkingSet} to be - * used in fixpoints. - * @param conf the {@link FixpointConfiguration} containing - * the parameters tuning fixpoint behavior + * @param entryState the entry state for the {@link CFG}s that are the + * entrypoints of the computation + * @param conf the {@link FixpointConfiguration} containing the + * parameters tuning fixpoint behavior * * @throws FixpointException if something goes wrong while evaluating the * fixpoint */ void fixpoint( AnalysisState entryState, - Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/collections/workset/OrderBasedWorkingSet.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/collections/workset/OrderBasedWorkingSet.java new file mode 100644 index 000000000..f41cdec77 --- /dev/null +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/collections/workset/OrderBasedWorkingSet.java @@ -0,0 +1,98 @@ +package it.unive.lisa.util.collections.workset; + +import it.unive.lisa.program.cfg.CodeLocation; +import it.unive.lisa.program.cfg.statement.Statement; +import java.util.Collection; +import java.util.Objects; +import java.util.SortedSet; +import java.util.TreeSet; + +/** + * A {@link WorkingSet} for {@link Statement}s that sorts its contents according + * to their natural order. This is specifically designed for fixpoint algorithms + * of CFGs: since the natural order of Statements discriminates for their + * {@link CodeLocation} first, this allows instructions that are exit points of + * control-flow structures to be analyzed only when all branches of the + * preceding structure has been fully analyzed. This holds since, unless several + * GOTO-like instructions are present, contents of ifs and loops always appear + * earlier in the code w.r.t. the exit points.
+ *
+ * Note that this working set is backed by a set: it is thus impossible to have + * duplicates in it. + * + * @author Luca Negrini + */ +public class OrderBasedWorkingSet implements WorkingSet { + + private final SortedSet ws; + + private OrderBasedWorkingSet() { + ws = new TreeSet<>(); + } + + /** + * Yields a new, empty working set. + * + * @return the new working set + */ + public static OrderBasedWorkingSet mk() { + return new OrderBasedWorkingSet(); + } + + @Override + public void push( + Statement e) { + ws.add(e); + } + + @Override + public Statement pop() { + Statement first = ws.first(); + ws.remove(first); + return first; + } + + @Override + public Statement peek() { + return ws.first(); + } + + @Override + public int size() { + return ws.size(); + } + + @Override + public boolean isEmpty() { + return ws.isEmpty(); + } + + @Override + public Collection getContents() { + return ws; + } + + @Override + public String toString() { + return ws.toString(); + } + + @Override + public int hashCode() { + return Objects.hash(ws); + } + + @Override + public boolean equals( + Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + OrderBasedWorkingSet other = (OrderBasedWorkingSet) obj; + return Objects.equals(ws, other.ws); + } + +} diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestInterproceduralAnalysis.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestInterproceduralAnalysis.java index 861cd1907..ea0bfa960 100644 --- a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestInterproceduralAnalysis.java +++ b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestInterproceduralAnalysis.java @@ -16,13 +16,11 @@ import it.unive.lisa.interprocedural.callgraph.CallResolutionException; import it.unive.lisa.program.Application; import it.unive.lisa.program.cfg.CFG; -import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.program.cfg.statement.call.CFGCall; import it.unive.lisa.program.cfg.statement.call.Call; import it.unive.lisa.program.cfg.statement.call.OpenCall; import it.unive.lisa.program.cfg.statement.call.UnresolvedCall; import it.unive.lisa.type.Type; -import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; import java.util.Collection; import java.util.Set; @@ -45,7 +43,6 @@ public void init( @Override public void fixpoint( AnalysisState entryState, - Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException { }