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

CFI update for Value inference to work with hack mode #285

Open
wants to merge 63 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
63 commits
Select commit Hold shift + click to select a range
8fadcc7
Added Z3smt solver
Sep 23, 2019
ca34b12
correct z3smt package name
Sep 24, 2019
87ddb4c
clean up debug code and unused code
txiang61 Oct 1, 2019
ad0f0f3
little format adjestment
txiang61 Oct 1, 2019
80048c4
eliminate one TODO
txiang61 Oct 4, 2019
26e5c06
Update .travis-build-without-test.sh
txiang61 Oct 7, 2019
8a7c31b
Update .travis-build-without-test.sh
txiang61 Oct 7, 2019
f7b2b91
Update .travis-build-without-test.sh
txiang61 Oct 7, 2019
6f9b878
Update .travis-build-without-test.sh
txiang61 Oct 7, 2019
658c3ee
added preference for subtype constraints to prefer constant slot over…
txiang61 Oct 8, 2019
b6dc6dd
restructure Z3SmtSolver so it can be overriden by both the unit-infer…
txiang61 Oct 17, 2019
c62dbc0
reformat Z3SmtConstraintEncoderFactory
txiang61 Oct 17, 2019
f068fc7
Added operation kind for comparable constraints encoder and its slot
txiang61 Oct 23, 2019
8f1669d
added underlying type to Variable Slot
txiang61 Nov 1, 2019
1f62945
removed comparable slot
txiang61 Nov 1, 2019
ea8d0a5
added underlying type to Variable Slot
txiang61 Nov 1, 2019
a1f8853
Addded unary and compount assginment handling in variable annotator
txiang61 Nov 7, 2019
8748fa2
improve javadoc in variable annotator for unary and compound assignme…
txiang61 Nov 7, 2019
692c126
Merge branch 'unary_compound'
txiang61 Nov 7, 2019
7476de4
Merge branch 'master' into add_variable_slot_type
xingweitian Nov 8, 2019
c1f65d1
Slot refactor. Make all slots that extends varaibleslot to extends sl…
txiang61 Nov 9, 2019
d31f22b
Merge branch 'add_variable_slot_type' of https://github.com/txiang61/…
txiang61 Nov 9, 2019
36fe6ed
Slot refactor. Make all slots that extends varaibleslot to extends sl…
txiang61 Nov 9, 2019
ad0c61d
Merge opprop master to this
txiang61 Nov 11, 2019
2193c77
Merge branch 'master' into add_z3
txiang61 Nov 11, 2019
d52c20f
slot refactoring. Remove all cast to VariableSlot and uses Slot instead
txiang61 Nov 11, 2019
30de4f6
slot refactoring. Remove all cast to VariableSlot and uses Slot instead
txiang61 Nov 11, 2019
07eb554
Merge branch 'master' of https://github.com/opprop/checker-framework-…
txiang61 Nov 12, 2019
abaeae7
add ArithmeticVariableSlot serialization and clean up some code
txiang61 Nov 14, 2019
9af2d34
add ArithmeticVariableSlot serialization and clean up some code
txiang61 Nov 14, 2019
b201b52
added Z3SmtSoftConstraintEncoder and moved all soft constraints encod…
txiang61 Nov 15, 2019
8bccb7d
update test files and correct variableslot insertion and utilize vari…
txiang61 Nov 15, 2019
9357851
Merge branch 'master' into add_variable_slot_type
txiang61 Nov 20, 2019
5908ead
Update Serializer.java
txiang61 Nov 20, 2019
23def40
Update CnfVecIntSerializer.java
txiang61 Nov 20, 2019
a6574c0
Update JsonSerializer.java
txiang61 Nov 20, 2019
e1a1850
Update ToStringSerializer.java
txiang61 Nov 20, 2019
cd33d90
Update PrintUtils.java
txiang61 Nov 20, 2019
0dea5d4
Merge pull request #1 from txiang61/add_variable_slot_type
txiang61 Nov 20, 2019
3364a49
Merge branch 'master' of https://github.com/txiang61/checker-framewor…
txiang61 Nov 20, 2019
5337de0
Merge remote-tracking branch 'opprop/master'
txiang61 Nov 20, 2019
95cbef7
Merge branch 'master' into add_z3
txiang61 Nov 20, 2019
4d28ec7
Merge pull request #2 from txiang61/add_z3
txiang61 Nov 20, 2019
a433be3
fix error
txiang61 Nov 20, 2019
57cd019
Change comparable constraint structure and rename operators
txiang61 Nov 21, 2019
4c0c314
create refinment slot when decalre variable with initialization
txiang61 Nov 24, 2019
d0e855e
create refinment slot when decalre variable with initialization
txiang61 Nov 24, 2019
4022263
Merge branch 'master' of https://github.com/txiang61/checker-framewor…
txiang61 Nov 28, 2019
c2fd065
create refinment variable for desugared trees since the desugared tre…
txiang61 Dec 11, 2019
59ac962
Update repo with changes in opprop/master
txiang61 Mar 22, 2020
9b3fd11
Merge remote-tracking branch 'opprop/master'
txiang61 Jul 19, 2020
9ddab04
Add comparison constraint instead of modifying comparable constriant …
txiang61 Jun 26, 2020
df85f55
clean up
txiang61 Jun 26, 2020
e5f6eeb
add variable slot create
txiang61 Jul 23, 2020
0b14f91
fixed problems with the comparison constraints
txiang61 Aug 19, 2020
0191dd1
hacks
txiang61 Aug 25, 2020
5132e87
add hacks to fix poly problem
txiang61 Sep 1, 2020
162066f
add hacks to avoid null pointer exceptions
txiang61 Sep 2, 2020
87514a1
fix refinement to get declared instead of comparison slot
txiang61 Sep 10, 2020
a6c1efd
fixed problems with the comparison constraints
txiang61 Aug 19, 2020
06e5e5e
fixed problems with the comparison constraints
txiang61 Aug 19, 2020
9c961c5
Merge remote-tracking branch 'opprop/master'
txiang61 Oct 13, 2020
8911126
Merge branch 'master' into value-benchmark
txiang61 Oct 13, 2020
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
eliminate one TODO
  • Loading branch information
txiang61 committed Oct 4, 2019

Verified

This commit was signed with the committer’s verified signature.
darkdh Anthony Tseng
commit 80048c415c07f1478e7236abb6e8abbedc9915f1
5 changes: 2 additions & 3 deletions src/checkers/inference/solver/backend/z3smt/Z3SmtSolver.java
Original file line number Diff line number Diff line change
@@ -283,15 +283,14 @@ protected void encodeAllConstraints() {
}

// generate a soft constraint that we prefer equality for subtype
// TODO: perhaps prefer not bottom and prefer not top will suffice?
if (optimizingMode && constraint instanceof SubtypeConstraint) {
SubtypeConstraint stc = (SubtypeConstraint) constraint;

Constraint eqc =
InferenceMain.getInstance()
.getConstraintManager()
.createEqualityConstraint(stc.getSubtype(), stc.getSupertype());

Expr simplifiedEQC = eqc.serialize(formatTranslator).simplify();

if (!simplifiedEQC.isTrue()) {