diff options
| author |  Unknown <afd@afd-THINK.home> | 2012-02-29 20:42:35 +0000 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.home> | 2012-02-29 20:42:35 +0000 |
| commit | 8f2f6d4a5a63a2e817e76422ebbab878a940351f (patch) | |
| tree | 5039eec37b2d69ede09ad802fef73c4608d6e887 /Source | |
| parent | 8a21671ed045957887b2170e9054a4814d4d1edc (diff) | |
Added missing files.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/GPUVerify/CrossThreadInvariantProcessor.cs | 42 | ||||
| -rw-r--r-- | Source/GPUVerify/EnabledToPredicateVisitor.cs | 39 |
2 files changed, 81 insertions, 0 deletions
diff --git a/Source/GPUVerify/CrossThreadInvariantProcessor.cs b/Source/GPUVerify/CrossThreadInvariantProcessor.cs new file mode 100644 index 00000000..b5772c0c --- /dev/null +++ b/Source/GPUVerify/CrossThreadInvariantProcessor.cs @@ -0,0 +1,42 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+
+namespace GPUVerify
+{
+ class CrossThreadInvariantProcessor : StandardVisitor
+ {
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+
+ if (node.Fun is FunctionCall)
+ {
+ FunctionCall call = node.Fun as FunctionCall;
+
+ if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool"))
+ {
+ return Expr.True;
+/* Debug.Assert(false);
+ return Expr.Eq(new VariableDualiser(1).VisitExpr(node.Args[0].Clone() as Expr),
+ new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr));*/
+ }
+
+ if (call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool"))
+ {
+ return Expr.Neq(new VariableDualiser(1).VisitExpr(node.Args[0].Clone() as Expr),
+ new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr));
+ }
+
+ }
+
+ return base.VisitNAryExpr(node);
+ }
+
+
+
+ }
+}
diff --git a/Source/GPUVerify/EnabledToPredicateVisitor.cs b/Source/GPUVerify/EnabledToPredicateVisitor.cs new file mode 100644 index 00000000..3cedd075 --- /dev/null +++ b/Source/GPUVerify/EnabledToPredicateVisitor.cs @@ -0,0 +1,39 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+
+namespace GPUVerify
+{
+ class EnabledToPredicateVisitor : StandardVisitor
+ {
+
+ public EnabledToPredicateVisitor(TypedIdent currentPredicate)
+ {
+ this.currentPredicate = currentPredicate;
+
+ }
+
+ private TypedIdent currentPredicate;
+
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ if (node.Fun is FunctionCall)
+ {
+ FunctionCall call = node.Fun as FunctionCall;
+
+ if (call.Func.Name.Equals("__enabled"))
+ {
+ return new IdentifierExpr(node.tok, new LocalVariable(node.tok, currentPredicate));
+ }
+
+ }
+
+ return base.VisitNAryExpr(node);
+ }
+
+ }
+}
|