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.

Sign up for GitHub

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

Fix simple-ltid.cu #661

Merged
merged 7 commits into from
Jul 19, 2021
Merged

Fix simple-ltid.cu #661

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
ff86330
Changes towards fixing simple-ltid.cu
bobismijnnaam Jul 15, 2021
78a480f
Move rewrite rule.
bobismijnnaam Jul 15, 2021
9b997ec
Only force frac type of literals.
bobismijnnaam Jul 15, 2021
289f7c0
Change perm frac arg to match against frac and not int
bobismijnnaam Jul 15, 2021
edb9e6d
In split2, match a frac, and not an int
bobismijnnaam Jul 15, 2021
b5e5695
Reduce the number of frac vars
bobismijnnaam Jul 16, 2021
e76a88a
Merge branch 'dev' into fix-simple-ltid
bobismijnnaam Jul 19, 2021
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
2 changes: 1 addition & 1 deletion examples/known-problems/gpgpu/simple-ltid.cu
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
//:: case SimpleLtid
//:: tools silicon
//:: suite problem-fail
//:: verdict Pass

#include <cuda.h>

Expand Down
8 changes: 6 additions & 2 deletions src/main/java/vct/col/util/AbstractTypeCheck.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1717,8 +1717,12 @@ private void force_frac(ASTNode arg) {
Warning("Encountered an integer division ('/') '%s' where a fraction was expected, did you mean a fraction division ('\\') here?", arg);
}

if(arg.getType().isPrimitive(PrimitiveSort.Integer)) {
arg.setType(new PrimitiveType(PrimitiveSort.Fraction));
if (arg instanceof ConstantExpression && arg.getType().isPrimitive(PrimitiveSort.Integer)) {
if (arg.equals(0)) {
arg.setType(new PrimitiveType(PrimitiveSort.ZFraction));
Vescatur marked this conversation as resolved.
Show resolved Hide resolved
} else {
arg.setType(new PrimitiveType(PrimitiveSort.Fraction));
}
}

if(arg instanceof OperatorExpression) {
Expand Down
13 changes: 10 additions & 3 deletions src/main/universal/res/config/simplify_quant_pass1.jspec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ class simplify_quant_pass1 {
int i,j,k;
rational p1,p2;
int tid;
frac f1;

axiom aunitr { e1+0 == e1 }
axiom aunitl { 0+e1 == e1 }
Expand All @@ -18,6 +19,7 @@ class simplify_quant_pass1 {
axiom I2 {
0 * e1 == 0
}

axiom I3 {
e1 * 0 == 0
}
Expand Down Expand Up @@ -159,7 +161,7 @@ class simplify_quant_pass1 {
// }

axiom perm_any {
Perm(ar[*],e1) == (\forall* int i_fresh ; 0 <= i_fresh && i_fresh < ar.length ; Perm(ar[i_fresh],e1))
Perm(ar[*],f1) == (\forall* int i_fresh ; 0 <= i_fresh && i_fresh < ar.length ; Perm(ar[i_fresh],f1))
}

axiom array_perm {
Expand Down Expand Up @@ -407,9 +409,9 @@ class simplify_quant_pass1 {
}

axiom split2 {
(\forall* int i;b1;PointsTo(e2,e3,e4))
(\forall* int i;b1;PointsTo(e2,f1,e4))
==
(\forall* int i;b1;Perm(e2,e3)) ** (\forall int i;b1;e2==e4)
(\forall* int i;b1;Perm(e2,f1)) ** (\forall int i;b1;e2==e4)
}

/* // SJ: unfortunately, this introduces an existential quantifier which is not always a good thing...
Expand Down Expand Up @@ -446,9 +448,14 @@ class simplify_quant_pass1 {
(\let int canary = i; i == 0 ? read : read)
}

// This rewrite rule causes some issues: https://github.com/viperproject/silicon/issues/539
axiom resource_independent_read_quant {
(\forall* int tid; (tid \memberof {e1..e2}); (Perm(g1, read)!tid))
==
(e1<e2) ==> Perm(g1, read)
}

// Using an int for the second argument of a perm is not allowed.
// Hence, we divide by 1 to turn it into a frac again.
axiom perm_fix_frac { Perm(g1, e1) == Perm(g1, e1 \ 1) }
}