Skip to content

Commit

Permalink
[opt] Fold {x == y} if {x} and {y} known-zero equivalent
Browse files Browse the repository at this point in the history
  • Loading branch information
titzer committed Feb 2, 2024
1 parent c719edc commit 13ad835
Show file tree
Hide file tree
Showing 8 changed files with 30 additions and 10 deletions.
2 changes: 1 addition & 1 deletion aeneas/src/main/Version.v3
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,6 @@

// Updated by VCS scripts. DO NOT EDIT.
component Version {
def version: string = "III-7.1682";
def version: string = "III-7.1683";
var buildData: string;
}
2 changes: 1 addition & 1 deletion aeneas/src/ssa/SsaOptimizer.v3
Original file line number Diff line number Diff line change
Expand Up @@ -384,7 +384,7 @@ class SsaInstrReducer(context: SsaContext) extends SsaInstrMatcher {
if (x == y) return graph.trueConst();
var and = x.facts & y.facts, or = x.facts | y.facts;
if (Facts.NONE != (and & Fact.V_ZERO)) return graph.trueConst(); // 0 == 0 == true
//TODO if (ZERO_NON_ZERO == (or & ZERO_NON_ZERO)) return graph.falseConst(); // 0 == nonzero == false
if (ZERO_NON_ZERO == (or & ZERO_NON_ZERO)) return graph.falseConst(); // 0 == nonzero == false
if (ABOVE_BELOW_ZERO == (or & ABOVE_BELOW_ZERO)) return graph.falseConst(); // neg == pos == false
}
VariantEq => {
Expand Down
5 changes: 5 additions & 0 deletions test/core/opt_nz00.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute 0=false; 1=false
def main(a: int) -> bool {
return (a | 1) == (a & 0);
}

7 changes: 3 additions & 4 deletions test/core/opt_nz01.v3
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
//@execute 0=false; 1=false
component opt_nz01 {
def main(a: int) -> bool {
return (a | 1) == 0;
}
def main(a: int) -> bool {
return (a | 1) == 0;
}

7 changes: 3 additions & 4 deletions test/core/opt_nz02.v3
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
//@execute 0=true; 1=true
component opt_nz02 {
def main(a: int) -> bool {
return (a | 1) != 0;
}
def main(a: int) -> bool {
return (a | 1) != 0;
}

5 changes: 5 additions & 0 deletions test/core/opt_nz03.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
//@execute 0=false; -1=false
def main(a: int) -> bool {
var x = if(a < 0, 1, 2);
return x == 0;
}
6 changes: 6 additions & 0 deletions test/core/opt_nz04.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute 0=false; -1=false
def main(a: int) -> bool {
var x = if(a < 0, 1, 2);
var y = if(a > 0, a & 0, x & 0);
return x == y;
}
6 changes: 6 additions & 0 deletions test/core/opt_nz05.v3
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
//@execute (0, 0)=true; (0, 1)=false; (1, 0)=false; (1, 1)=true
def main(a: int, b: int) -> bool {
var x = if(a != 0, 1, 0);
var y = if(b != 0, 1, 0);
return x == y;
}

0 comments on commit 13ad835

Please sign in to comment.