Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Sleep-Reduced Thread-Modular Proofs and related CHC refactoring #701

Draft
wants to merge 123 commits into
base: dev
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
123 commits
Select commit Hold shift + click to select a range
8a7e125
IcfgToChcConcurrent: some documentation and minor refactoring
maul-esel Apr 1, 2023
ce90413
begin (very hacky) support for sleep sets in Horn clauses
maul-esel Apr 4, 2023
f9675a1
add common interface for variables specific to a thread instance
maul-esel Apr 4, 2023
ddc58b6
more simplification with ThreadInstance
maul-esel Apr 4, 2023
7d637c5
new implementation of Horn clause generation for thread-modular proofs
maul-esel Apr 5, 2023
db0f9e5
fix Horn clauses with non-false head
maul-esel Apr 5, 2023
053b755
add support for variables not tied to a specific predicate and index
maul-esel Apr 5, 2023
10f4bfc
fix location constraint
maul-esel Apr 5, 2023
83e5dca
refactor ChcProviderConcurrentWithLbe: create new ICFG, use existing …
maul-esel Apr 5, 2023
5b7e3f0
add mode and level parameters to ChcProviderConcurrent
maul-esel Apr 5, 2023
a50b4e5
add BidirectionalMap::merge (allows to be used in stream collectors)
maul-esel Apr 11, 2023
e450ef4
HcSymbolTable fix copy-paste error
maul-esel Apr 11, 2023
366c858
continue refactoring
maul-esel Apr 11, 2023
3a232af
make sleep set vars boolean
maul-esel Apr 11, 2023
1056ed1
Merge branch 'dev' into wip/dk/sleep-threadmodular
maul-esel Apr 18, 2023
eb16dfe
IcfgToChc: add preferences
maul-esel Apr 18, 2023
77aeaca
extract ConcurrencyMode functionality
maul-esel Apr 18, 2023
b6359ad
refactor Horn clause generation
maul-esel Apr 18, 2023
dc6408f
remove obsolete code
maul-esel Apr 18, 2023
f510f23
add missing license header
maul-esel Apr 18, 2023
247528e
implement support for pre-/postconditions
maul-esel Apr 19, 2023
f10639e
separate ability to specify preconditions from spec mode
maul-esel Apr 20, 2023
3cf5dbc
IHcReplacementVar: consistently give Script not Sort
maul-esel May 8, 2023
bc239dc
add interface for finite-valued variables, and implement for HcSleepVar
maul-esel May 8, 2023
0493755
PredicateInfo: drop bidirectional map, simplify code
maul-esel May 8, 2023
1a5620f
add small optimization: drop Horn clauses with constraint false
maul-esel May 8, 2023
95355cc
add predicate families, to prepare support for different encodings
maul-esel May 9, 2023
a7f57b1
add settings for future encoding variants
maul-esel May 9, 2023
85aa4c4
add setting for different preference order encoding
maul-esel May 9, 2023
4114dde
IHcThreadSpecificVar: add forInstance method
maul-esel May 10, 2023
65b7c63
fix IcfgToChc preferences, output more detailed error in the future
maul-esel May 10, 2023
721589e
another fix for settings code
maul-esel May 10, 2023
9aa0c92
HcSleepVar: properly implement forInstance
maul-esel May 10, 2023
c78c7c0
SleepSetThreadModularProofs: properly implement symmetry breaking
maul-esel May 10, 2023
6552ec7
SleepSetThreadModular w/o symmetry-breaking: simplify code slightly
maul-esel May 10, 2023
7e3d4fa
fix transition constraints for local variables
maul-esel May 17, 2023
611e7b9
add alternative assert encoding
maul-esel May 17, 2023
eff6fbf
Merge branch 'dev' into wip/dk/sleep-threadmodular
maul-esel May 20, 2023
5535543
Fix NPE
schuessf May 23, 2023
3568919
Fix NPE properly
schuessf May 23, 2023
0e06dcb
add some comments
maul-esel May 24, 2023
71759d3
create new package for POR-related classes
maul-esel May 24, 2023
bb52355
add auxiliary method for skippable asserts
maul-esel May 24, 2023
07ae11c
fix handling of local variables
maul-esel May 24, 2023
da5fb75
Merge branch 'dev' into wip/dk/sleep-threadmodular
maul-esel May 24, 2023
352794a
readable toString for dummy edges (to help debugging)
maul-esel May 25, 2023
6a47de5
SemanticIndependenceConditionGenerator: also output raw terms
maul-esel May 25, 2023
6c22120
add SemanticIndependenceConditionGenerator::isSymmetric
maul-esel May 25, 2023
81cfd05
HcSymbolTable: add missing mapping of head variables
maul-esel May 25, 2023
f838715
add support for conditional independence (with precomputed commutativ…
maul-esel May 25, 2023
e388a02
minor preference cleanup: put sleep set settings in container
maul-esel May 25, 2023
ef5fd25
move CHC categorization to its own class
maul-esel May 25, 2023
3b0b011
simpler postcondition encoding: only one thread counter
maul-esel May 25, 2023
9a82c70
implement support for different preference orders
maul-esel May 25, 2023
23ac64f
Merge branch 'dev' into wip/dk/sleep-threadmodular
maul-esel May 25, 2023
d18db27
ChcSmtPrinter: use configured file name as prefix for automatic naming
maul-esel May 25, 2023
9bb4800
IndependenceChecker: properly substitute global variables
maul-esel May 25, 2023
b12de36
better checking of CHCs
maul-esel May 25, 2023
bf2c225
Merge branch 'dev' into wip/dk/sleep-threadmodular
maul-esel May 25, 2023
621497e
fix copy-paste error
maul-esel May 26, 2023
fe2097d
add setting to allow semi-commutativity (default: true)
maul-esel May 26, 2023
d5022d5
prepare evaluation
maul-esel May 31, 2023
cab6167
fix usage of benchexec variables
maul-esel May 31, 2023
b79fc11
add golem during build
maul-esel May 31, 2023
30509f9
TreeAutomizer: must not use Z3 (no longer supports interpolation)
maul-esel May 31, 2023
645efe7
temporarily disable check that crashes UniHorn
maul-esel May 31, 2023
4f2efde
Merge branch 'dev' into wip/dk/sleep-threadmodular
maul-esel Jun 6, 2023
ff2fe87
improve Z3 CHC integration
maul-esel Jun 6, 2023
1f01ed6
SmtChcScript: avoid push/pop
maul-esel Jun 7, 2023
27c56ed
fix typos in method names
maul-esel Jun 8, 2023
7dddfbb
bugfix: record HcBodyVar for each term variable
maul-esel Jun 8, 2023
15814dd
construct HcHeadVars that reference the proper predicate and index
maul-esel Jun 8, 2023
dca59fe
eldarica: properly handle scala objects
maul-esel Jun 8, 2023
7573845
fix SMT solver setting: TreeAutomizer ignores its own settings
maul-esel Jun 8, 2023
a13f12b
add an IChcScript to invoke eldarica via command line
maul-esel Jun 9, 2023
968a270
log model if found
maul-esel Jun 9, 2023
011ae38
ChcTransferrer: fix resolution of head variables
maul-esel Jun 9, 2023
d2af6b7
ChcTransferrer: implement transferBack(Model)
maul-esel Jun 9, 2023
3a8dd60
prepare more extensive evaluation
maul-esel Jun 12, 2023
bc7f6ac
ChcTransferrer: fix model backtranslation
maul-esel Jun 13, 2023
e6bf6e3
ApproximateLockstepPreferenceOrder: do not confuse locations with the…
maul-esel Jun 15, 2023
e9a7c2e
fix implementation of thread-modular preference orders
maul-esel Jun 15, 2023
66e461b
add setting for SKIP_ASSERTION_EDGES
maul-esel Jun 16, 2023
806d74d
ensure models are in Ultimate normal form
maul-esel Jun 16, 2023
90a251a
temporarily (for evaluation) avoid let terms in models
maul-esel Jun 16, 2023
f271ee5
SmtChcScript: transfer models to the proper script
maul-esel Jun 16, 2023
c8ff3af
throw error for joins even without -ea
maul-esel Jun 21, 2023
78f4435
parametric programs: support multiple templates and single-instance t…
maul-esel Jun 22, 2023
a63ceb3
fix pre/post detection for multiple templates
maul-esel Jun 22, 2023
c5b3d18
skip error locations if "skip assert edges" enabled
maul-esel Jun 24, 2023
ccadede
properly filter error locs from CHC system
maul-esel Jun 28, 2023
fa7c491
fix order for semicommutativity
maul-esel Jun 28, 2023
1b43378
more work on pre/post for parametric programs
maul-esel Jun 28, 2023
74fdd48
Merge branch 'dev' into wip/dk/sleep-threadmodular
maul-esel Jun 29, 2023
5ab1b01
temporarily hardcode some conditions for eval purposes
maul-esel Jul 3, 2023
436ddf1
remove unused variable
maul-esel Jul 22, 2023
98c31e4
Merge branch 'dev' into wip/dk/sleep-threadmodular
maul-esel Sep 8, 2023
25ec55f
mark unimplemented settings
maul-esel Sep 8, 2023
7112670
small settings cleanup
maul-esel Sep 11, 2023
4561965
add setting for symmetry clauses
maul-esel Sep 11, 2023
dcd3a62
prepare evaluation with symmetry clauses
maul-esel Sep 11, 2023
b633ca1
fix NullPointerException for clause without constraint
maul-esel Sep 12, 2023
6de61bb
HornClause: remove unused ManagedScript parameter
maul-esel Sep 12, 2023
dd9be67
prepare evaluation
maul-esel Sep 12, 2023
4130816
prepare evaluation of yet-unsolved tasks
maul-esel Sep 13, 2023
f799994
ChcSolver: support passing predicate hints to eldarica
maul-esel Sep 14, 2023
d7d68cd
Merge branch 'dev' into wip/dk/sleep-threadmodular
maul-esel Dec 11, 2024
2ffed63
add test suite for thread-modular proofs with sleep set reduction
maul-esel Dec 11, 2024
9d47071
switch to new ISymbolicIndependenceRelation
maul-esel Dec 12, 2024
a0c725d
IndependenceChecker: decouple from HornClauseBuilder
maul-esel Dec 12, 2024
a1d3017
fix assert failure for clauses without head (safety clauses)
maul-esel Dec 12, 2024
e5f34f8
fix bug with unknown variables in predicate factory
maul-esel Dec 12, 2024
921d0ad
remove hardcoded commutativity conditions (reverts 5ab1b01)
maul-esel Dec 12, 2024
21e81a6
SleepThreadModularChcTestSuite: specify solver in task definition
maul-esel Dec 12, 2024
4aa7bf4
remove some redundant tests, fix expected timeout
maul-esel Dec 13, 2024
019bfb4
add setting for nondeterministic sleep updates
maul-esel Dec 19, 2024
07d3146
prepare evaluation
maul-esel Dec 19, 2024
2d603c6
fix path
maul-esel Dec 19, 2024
3f1e3e5
fix benchmark file: command line parameters
maul-esel Dec 30, 2024
85b1de3
undo temporary debugging changes
maul-esel Jan 3, 2025
52675bb
remove EldaricaChcScript and related classes (for now)
maul-esel Jan 7, 2025
ca714d1
improvements to IHcReplacementVar implementations
maul-esel Jan 7, 2025
972bd96
add missing benchmark rundefinitions
maul-esel Jan 8, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
PredicateInfo: drop bidirectional map, simplify code
maul-esel committed May 8, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 049375592b2ce6f692f20773fd2a6da70512430d
Original file line number Diff line number Diff line change
@@ -33,7 +33,6 @@
import java.util.Map;
import java.util.Set;
import java.util.stream.Collectors;
import java.util.stream.IntStream;

import de.uni_freiburg.informatik.ultimate.lib.chc.HcBodyVar;
import de.uni_freiburg.informatik.ultimate.lib.chc.HcHeadVar;
@@ -98,8 +97,7 @@ public void differentBodyHeadVar(final IHcReplacementVar variable) {
}

public List<Term> getDefaultBodyArgs(final PredicateInfo predicate) {
return IntStream.range(0, predicate.getParamCount())
.mapToObj(i -> getBodyVar(predicate.getParameter(i)).getTerm())
return predicate.getParameters().stream().map(param -> getBodyVar(param).getTerm())
.collect(Collectors.toCollection(ArrayList::new));
}

@@ -126,8 +124,8 @@ public HornClause build() {
clause = new HornClause(mManagedScript, mSymbolTable, constraint, mBodyPreds, substitutedBodyArgs,
mBodyVars);
} else {
final var headArgs = IntStream.range(0, mHeadPredicate.getParamCount())
.mapToObj(i -> getHeadVar(mHeadPredicate.getParameter(i))).collect(Collectors.toList());
final var headArgs =
mHeadPredicate.getParameters().stream().map(this::getHeadVar).collect(Collectors.toList());
clause = new HornClause(mManagedScript, mSymbolTable, constraint, mHeadPredicate.getPredicate(), headArgs,
mBodyPreds, substitutedBodyArgs, mBodyVars);
}
@@ -143,8 +141,7 @@ private void prepareSubstitution() {
}

mSubstitution.clear();
for (int i = 0; i < mHeadPredicate.getParamCount(); ++i) {
final var variable = mHeadPredicate.getParameter(i);
for (final var variable : mHeadPredicate.getParameters()) {
if (!mModifiedVars.contains(variable)) {
mSubstitution.put(getBodyVar(variable).getTermVariable(), getHeadVar(variable).getTerm());
}
Original file line number Diff line number Diff line change
@@ -26,47 +26,40 @@
*/
package de.uni_freiburg.informatik.ultimate.plugins.icfgtochc.concurrent;

import java.util.Collection;
import java.util.List;
import java.util.Objects;

import de.uni_freiburg.informatik.ultimate.lib.chc.HcPredicateSymbol;
import de.uni_freiburg.informatik.ultimate.util.datastructures.BidirectionalMap;

public class PredicateInfo {
private final HcPredicateSymbol mPredicate;
private final BidirectionalMap<IHcReplacementVar, Integer> mVariable2Index;
protected final List<IHcReplacementVar> mParameters;

public PredicateInfo(final HcPredicateSymbol predicate,
final BidirectionalMap<IHcReplacementVar, Integer> variable2Index) {
public PredicateInfo(final HcPredicateSymbol predicate, final List<IHcReplacementVar> parameters) {
mPredicate = predicate;
mVariable2Index = variable2Index;
mParameters = parameters;
}

public HcPredicateSymbol getPredicate() {
return mPredicate;
}

public boolean hasParameter(final IHcReplacementVar variable) {
return mVariable2Index.containsKey(variable);
}

public int getIndex(final IHcReplacementVar variable) {
assert mVariable2Index.containsKey(variable);
return mVariable2Index.get(variable);
public Collection<IHcReplacementVar> getParameters() {
return mParameters;
}

public IHcReplacementVar getParameter(final int index) {
final var result = mVariable2Index.inverse().get(index);
assert result != null : "No parameter at index " + index + " (out of " + mPredicate.getArity() + ")";
return result;
public boolean hasParameter(final IHcReplacementVar variable) {
return mParameters.contains(variable);
}

public int getParamCount() {
return mVariable2Index.size();
return mParameters.size();
}

@Override
public int hashCode() {
return Objects.hash(mPredicate, mVariable2Index);
return Objects.hash(mPredicate, mParameters);
}

@Override
@@ -81,6 +74,6 @@ public boolean equals(final Object obj) {
return false;
}
final PredicateInfo other = (PredicateInfo) obj;
return Objects.equals(mPredicate, other.mPredicate) && Objects.equals(mVariable2Index, other.mVariable2Index);
return Objects.equals(mPredicate, other.mPredicate) && Objects.equals(mParameters, other.mParameters);
}
}
Original file line number Diff line number Diff line change
@@ -29,6 +29,7 @@

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
@@ -37,7 +38,6 @@
import java.util.Set;
import java.util.function.Predicate;
import java.util.stream.Collectors;
import java.util.stream.IntStream;
import java.util.stream.Stream;

import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
@@ -62,7 +62,6 @@
import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
import de.uni_freiburg.informatik.ultimate.plugins.icfgtochc.preferences.IcfgToChcPreferences;
import de.uni_freiburg.informatik.ultimate.plugins.icfgtochc.preferences.IcfgToChcPreferences.SpecMode;
import de.uni_freiburg.informatik.ultimate.util.datastructures.BidirectionalMap;
import de.uni_freiburg.informatik.ultimate.util.datastructures.DataStructureUtils;
import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.NestedMap2;
import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair;
@@ -168,10 +167,7 @@ private PredicateInfo createInvariantPredicate() {
final List<Sort> sorts = parameters.stream().map(IHcReplacementVar::getSort).collect(Collectors.toList());
final var predicate = mSymbolTable.getOrConstructHornClausePredicateSymbol(FUNCTION_NAME, sorts);

final var paramMap = IntStream.range(0, parameters.size()).mapToObj(i -> new Pair<>(parameters.get(i), i))
.collect(Collectors.toMap(Pair::getKey, Pair::getValue, (i, j) -> i, BidirectionalMap::new));

return new PredicateInfo(predicate, paramMap);
return new PredicateInfo(predicate, parameters);
}

/**
@@ -549,10 +545,11 @@ protected HornClauseBuilder buildNonInterferenceClause(final IIcfgTransition<?>
final var interferingVars = createThreadSpecificVars(interferingThread);
for (int i = 0; i < instanceVars.size(); ++i) {
final var original = instanceVars.get(i);
final var replaced = interferingVars.get(i);
if (mInvariantPredicate.hasParameter(original)) {
final int index = mInvariantPredicate.getIndex(original);
bodyArgs.set(index, clause.getBodyVar(replaced).getTerm());
final var originalTerm = clause.getBodyVar(original).getTerm();
final var replaced = interferingVars.get(i);
final var replacedTerm = clause.getBodyVar(replaced).getTerm();
Collections.replaceAll(bodyArgs, originalTerm, replacedTerm);
}
}