From ff863306188733015c20fa6da8669d47856cad9d Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Thu, 15 Jul 2021 14:09:40 +0200 Subject: [PATCH 1/6] Changes towards fixing simple-ltid.cu A rewrite rule is added which ensures that any permission that gets written to Perm(field, integerExpression) gets rewritten to Perm(field, fracExpression). Previously the rewrite system could produce terms that were not well-typed (i.e. produced non-well-typed terms). simple-ltid.cu is also removed from suite problem-fail. --- examples/gpgpu/simple-ltid.cu | 2 +- src/main/universal/res/config/simplify_quant_pass1.jspec | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/examples/gpgpu/simple-ltid.cu b/examples/gpgpu/simple-ltid.cu index f5f310b51d..0cdba131a8 100644 --- a/examples/gpgpu/simple-ltid.cu +++ b/examples/gpgpu/simple-ltid.cu @@ -1,6 +1,6 @@ //:: case SimpleLtid //:: tools silicon -//:: suite problem-fail +//:: verdict Pass #include diff --git a/src/main/universal/res/config/simplify_quant_pass1.jspec b/src/main/universal/res/config/simplify_quant_pass1.jspec index 6b52931e9d..f5644448be 100644 --- a/src/main/universal/res/config/simplify_quant_pass1.jspec +++ b/src/main/universal/res/config/simplify_quant_pass1.jspec @@ -15,9 +15,14 @@ class simplify_quant_pass1 { axiom munitr { e1*1 == e1 } axiom munitl { 1*e1 == e1 } + // 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) } + axiom I2 { 0 * e1 == 0 } + axiom I3 { e1 * 0 == 0 } From 78a480f9425d5819d3635ec06010b00e8903ac7f Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Thu, 15 Jul 2021 14:43:39 +0200 Subject: [PATCH 2/6] Move rewrite rule. The rule perm_fix_frac is moved to the end as it seems to interefere with applying the rule for Perm(xs[*], e1). Doing it later should still work, and not interfere with the rule for xs[*]. --- src/main/universal/res/config/simplify_quant_pass1.jspec | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/main/universal/res/config/simplify_quant_pass1.jspec b/src/main/universal/res/config/simplify_quant_pass1.jspec index f5644448be..7d98a52b3b 100644 --- a/src/main/universal/res/config/simplify_quant_pass1.jspec +++ b/src/main/universal/res/config/simplify_quant_pass1.jspec @@ -15,10 +15,6 @@ class simplify_quant_pass1 { axiom munitr { e1*1 == e1 } axiom munitl { 1*e1 == e1 } - // 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) } - axiom I2 { 0 * e1 == 0 } @@ -451,9 +447,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 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) } } From 9b997ec32e62aa9e76662b6dd60d9fd18b9c956f Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Thu, 15 Jul 2021 16:06:30 +0200 Subject: [PATCH 3/6] Only force frac type of literals. Previously the typechecker would force the secon argument of a Perm to be frac. This would cause the rewriter to rewrite an int variable as a frac. We narrow this to only forcing literals to be frac, and leave all other types as they are. This ensures expressions like "read" are not matched against rewrite matching variables of type int. --- src/main/java/vct/col/util/AbstractTypeCheck.java | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/main/java/vct/col/util/AbstractTypeCheck.java b/src/main/java/vct/col/util/AbstractTypeCheck.java index 16f636edcc..acacb17d88 100644 --- a/src/main/java/vct/col/util/AbstractTypeCheck.java +++ b/src/main/java/vct/col/util/AbstractTypeCheck.java @@ -1706,8 +1706,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)); + } else { + arg.setType(new PrimitiveType(PrimitiveSort.Fraction)); + } } if(arg instanceof OperatorExpression) { From 289f7c056a21b118563634e68932a7c76025e056 Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Thu, 15 Jul 2021 16:27:26 +0200 Subject: [PATCH 4/6] Change perm frac arg to match against frac and not int --- src/main/universal/res/config/simplify_quant_pass1.jspec | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/universal/res/config/simplify_quant_pass1.jspec b/src/main/universal/res/config/simplify_quant_pass1.jspec index 7d98a52b3b..76f987d79c 100644 --- a/src/main/universal/res/config/simplify_quant_pass1.jspec +++ b/src/main/universal/res/config/simplify_quant_pass1.jspec @@ -8,6 +8,7 @@ class simplify_quant_pass1 { int i,j,k; rational p1,p2; int tid; + frac f1, f2, f3, f4; axiom aunitr { e1+0 == e1 } axiom aunitl { 0+e1 == e1 } @@ -160,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 { From edb9e6daf28f9b0a6b87482d97c92aead775871d Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Thu, 15 Jul 2021 16:56:26 +0200 Subject: [PATCH 5/6] In split2, match a frac, and not an int --- src/main/universal/res/config/simplify_quant_pass1.jspec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/universal/res/config/simplify_quant_pass1.jspec b/src/main/universal/res/config/simplify_quant_pass1.jspec index 76f987d79c..94b62798a9 100644 --- a/src/main/universal/res/config/simplify_quant_pass1.jspec +++ b/src/main/universal/res/config/simplify_quant_pass1.jspec @@ -409,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... From b5e569551ebc512dfb93e594597e9f3888f5e1b4 Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Fri, 16 Jul 2021 15:48:17 +0200 Subject: [PATCH 6/6] Reduce the number of frac vars --- src/main/universal/res/config/simplify_quant_pass1.jspec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/universal/res/config/simplify_quant_pass1.jspec b/src/main/universal/res/config/simplify_quant_pass1.jspec index 94b62798a9..c2e117a697 100644 --- a/src/main/universal/res/config/simplify_quant_pass1.jspec +++ b/src/main/universal/res/config/simplify_quant_pass1.jspec @@ -8,7 +8,7 @@ class simplify_quant_pass1 { int i,j,k; rational p1,p2; int tid; - frac f1, f2, f3, f4; + frac f1; axiom aunitr { e1+0 == e1 } axiom aunitl { 0+e1 == e1 }