-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #85 from ftsrg/cfaprop
Make error loc of CFA optional, add errorloc argument to CLI tool
- Loading branch information
Showing
16 changed files
with
211 additions
and
67 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
98 changes: 98 additions & 0 deletions
98
subprojects/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/EncodingTest.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,98 @@ | ||
| package hu.bme.mit.theta.cfa.analysis; | ||
|
|
||
| import com.google.common.collect.ImmutableSet; | ||
| import hu.bme.mit.theta.analysis.expr.ExprState; | ||
| import hu.bme.mit.theta.cfa.CFA; | ||
| import hu.bme.mit.theta.cfa.analysis.lts.CfaLbeLts; | ||
| import hu.bme.mit.theta.cfa.analysis.lts.CfaLts; | ||
| import hu.bme.mit.theta.cfa.analysis.lts.CfaSbeLts; | ||
| import hu.bme.mit.theta.cfa.dsl.CfaDslManager; | ||
| import hu.bme.mit.theta.core.type.Expr; | ||
| import hu.bme.mit.theta.core.type.booltype.BoolType; | ||
| import org.junit.Assert; | ||
| import org.junit.Before; | ||
| import org.junit.Test; | ||
|
|
||
| import java.io.FileInputStream; | ||
| import java.io.IOException; | ||
| import java.util.HashSet; | ||
| import java.util.Set; | ||
|
|
||
| public class EncodingTest { | ||
|
|
||
| private CFA cfa; | ||
|
|
||
| private CFA.Loc getLocByName(String name) { | ||
| for (CFA.Loc loc : cfa.getLocs()) { | ||
| if (loc.getName().equals(name)) return loc; | ||
| } | ||
| throw new IllegalArgumentException("Location not found"); | ||
| } | ||
|
|
||
| private Set<String> getNextLocs(CfaLts lts, String loc) { | ||
| Set<String> locs = new HashSet<>(); | ||
| SS ss = new SS(); | ||
| for (var act : lts.getEnabledActionsFor(CfaState.of(getLocByName(loc), ss))) { | ||
| locs.add(act.getTarget().getName()); | ||
| } | ||
| return locs; | ||
| } | ||
|
|
||
| private class SS implements ExprState { | ||
| @Override | ||
| public boolean isBottom() { | ||
| return false; | ||
| } | ||
|
|
||
| @Override | ||
| public Expr<BoolType> toExpr() { | ||
| return null; | ||
| } | ||
| } | ||
|
|
||
| @Before | ||
| public void load() throws IOException { | ||
| try (var fis = new FileInputStream("src/test/resources/block-encoding.cfa")) { | ||
| cfa = CfaDslManager.createCfa(fis); | ||
| } | ||
| } | ||
|
|
||
| @Test | ||
| public void testSbe() { | ||
| CfaSbeLts lts = CfaSbeLts.getInstance(); | ||
| Assert.assertEquals(ImmutableSet.of("L1"), getNextLocs(lts, "L0")); | ||
| Assert.assertEquals(ImmutableSet.of("L2", "L4"), getNextLocs(lts, "L1")); | ||
| Assert.assertEquals(ImmutableSet.of("L3"), getNextLocs(lts, "L2")); | ||
| Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L3")); | ||
| Assert.assertEquals(ImmutableSet.of("L5"), getNextLocs(lts, "L4")); | ||
| Assert.assertEquals(ImmutableSet.of("L1", "L6"), getNextLocs(lts, "L5")); | ||
| Assert.assertEquals(ImmutableSet.of("L7"), getNextLocs(lts, "L6")); | ||
| Assert.assertEquals(ImmutableSet.of(), getNextLocs(lts, "L7")); | ||
| } | ||
|
|
||
| @Test | ||
| public void testLbe1() { | ||
| CfaLbeLts lts = CfaLbeLts.of(getLocByName("L7")); | ||
| Assert.assertEquals(ImmutableSet.of("L1"), getNextLocs(lts, "L0")); | ||
| Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L1")); | ||
| Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L2")); | ||
| Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L3")); | ||
| Assert.assertEquals(ImmutableSet.of("L5"), getNextLocs(lts, "L4")); | ||
| Assert.assertEquals(ImmutableSet.of("L1", "L7"), getNextLocs(lts, "L5")); | ||
| Assert.assertEquals(ImmutableSet.of("L7"), getNextLocs(lts, "L6")); | ||
| Assert.assertEquals(ImmutableSet.of(), getNextLocs(lts, "L7")); | ||
| } | ||
|
|
||
| @Test | ||
| public void testLbe2() { | ||
| CfaLbeLts lts = CfaLbeLts.of(getLocByName("L3")); | ||
| Assert.assertEquals(ImmutableSet.of("L1"), getNextLocs(lts, "L0")); | ||
| Assert.assertEquals(ImmutableSet.of("L3", "L4"), getNextLocs(lts, "L1")); | ||
| Assert.assertEquals(ImmutableSet.of("L3"), getNextLocs(lts, "L2")); | ||
| Assert.assertEquals(ImmutableSet.of("L4"), getNextLocs(lts, "L3")); | ||
| Assert.assertEquals(ImmutableSet.of("L5"), getNextLocs(lts, "L4")); | ||
| Assert.assertEquals(ImmutableSet.of("L1", "L7"), getNextLocs(lts, "L5")); | ||
| Assert.assertEquals(ImmutableSet.of("L7"), getNextLocs(lts, "L6")); | ||
| Assert.assertEquals(ImmutableSet.of(), getNextLocs(lts, "L7")); | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
20 changes: 20 additions & 0 deletions
20
subprojects/cfa-analysis/src/test/resources/block-encoding.cfa
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| main process cfa { | ||
| init loc L0 | ||
| loc L1 | ||
| loc L2 | ||
| loc L3 | ||
| loc L4 | ||
| loc L5 | ||
| loc L6 | ||
| loc L7 | ||
|
|
||
| L0 -> L1 { } | ||
| L1 -> L2 { } | ||
| L2 -> L3 { } | ||
| L3 -> L4 { } | ||
| L1 -> L4 { } | ||
| L4 -> L5 { } | ||
| L5 -> L6 { } | ||
| L6 -> L7 { } | ||
| L5 -> L1 { } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.