diff options
| author |  stefanheule <unknown> | 2012-03-09 02:33:36 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-03-09 02:33:36 -0800 |
| commit | 1edc06c71b783d4a70d3e0e8a011fc47e78d3c3a (patch) | |
| tree | c0cd27c346d06c7111f6ae6e127cfae8e7fadac2 /Source/GPUVerify/AccessInvariantProcessor.cs | |
| parent | 55b69a7c7d029c9fbd607f563ecd23087141b298 (diff) | |
| parent | 68f2b9caf8b5d64399eb8e74daf75788bec74e4f (diff) | |
Automatic merge.
Diffstat (limited to 'Source/GPUVerify/AccessInvariantProcessor.cs')
| -rw-r--r-- | Source/GPUVerify/AccessInvariantProcessor.cs | 107 |
1 files changed, 107 insertions, 0 deletions
diff --git a/Source/GPUVerify/AccessInvariantProcessor.cs b/Source/GPUVerify/AccessInvariantProcessor.cs new file mode 100644 index 00000000..4a5c34e8 --- /dev/null +++ b/Source/GPUVerify/AccessInvariantProcessor.cs @@ -0,0 +1,107 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+
+namespace GPUVerify
+{
+ class AccessInvariantProcessor : StandardVisitor
+ {
+
+ private const string NO_READ = "__no_read_";
+ private const string NO_WRITE = "__no_write_";
+ private const string READ = "__read_";
+ private const string WRITE = "__write_";
+ private const string READ_OFFSET = "__read_offset_";
+ private const string WRITE_OFFSET = "__write_offset_";
+ private const string READ_IMPLIES = "__read_implies_";
+ private const string WRITE_IMPLIES = "__write_implies_";
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+
+ if (node.Fun is FunctionCall)
+ {
+ FunctionCall call = node.Fun as FunctionCall;
+
+ if (MatchesIntrinsic(call.Func, NO_READ))
+ {
+ return Expr.Not(
+ MakeReadHasOccurred(node, call, NO_READ)
+ );
+ }
+
+ if (MatchesIntrinsic(call.Func, NO_WRITE))
+ {
+ return Expr.Not(
+ MakeWriteHasOccurred(node, call, NO_WRITE)
+ );
+ }
+
+ if (MatchesIntrinsic(call.Func, READ_OFFSET))
+ {
+ return new IdentifierExpr(node.tok, new GlobalVariable(
+ node.tok, new TypedIdent(node.tok, "_READ_OFFSET_X_" +
+ call.Func.Name.Substring(READ_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32)))
+ );
+ }
+
+ if (MatchesIntrinsic(call.Func, WRITE_OFFSET))
+ {
+ return new IdentifierExpr(node.tok, new GlobalVariable(
+ node.tok, new TypedIdent(node.tok, "_WRITE_OFFSET_X_" +
+ call.Func.Name.Substring(WRITE_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32)))
+ );
+ }
+
+ if (MatchesIntrinsic(call.Func, READ))
+ {
+ return MakeReadHasOccurred(node, call, READ);
+ }
+
+ if (MatchesIntrinsic(call.Func, WRITE))
+ {
+ return MakeWriteHasOccurred(node, call, WRITE);
+ }
+
+ if (MatchesIntrinsic(call.Func, READ_IMPLIES))
+ {
+ return Expr.Imp(MakeReadHasOccurred(node, call, READ_IMPLIES), node.Args[0]);
+ }
+
+ if (MatchesIntrinsic(call.Func, WRITE_IMPLIES))
+ {
+ return Expr.Imp(MakeWriteHasOccurred(node, call, WRITE_IMPLIES), node.Args[0]);
+ }
+
+ }
+
+ return base.VisitNAryExpr(node);
+ }
+
+ private static IdentifierExpr MakeReadHasOccurred(NAryExpr node, FunctionCall call, string intrinsicPrefix)
+ {
+ return new IdentifierExpr(node.tok, new GlobalVariable(
+ node.tok, new TypedIdent(node.tok, "_READ_HAS_OCCURRED_" +
+ call.Func.Name.Substring(intrinsicPrefix.Length), Microsoft.Boogie.Type.Bool)));
+ }
+
+ private static IdentifierExpr MakeWriteHasOccurred(NAryExpr node, FunctionCall call, string intrinsicPrefix)
+ {
+ return new IdentifierExpr(node.tok, new GlobalVariable(
+ node.tok, new TypedIdent(node.tok, "_WRITE_HAS_OCCURRED_" +
+ call.Func.Name.Substring(intrinsicPrefix.Length), Microsoft.Boogie.Type.Bool)));
+ }
+
+
+ private bool MatchesIntrinsic(Function function, string intrinsicPrefix)
+ {
+ return function.Name.Length > intrinsicPrefix.Length &&
+ function.Name.Substring(0, intrinsicPrefix.Length).Equals(intrinsicPrefix);
+ }
+
+
+ }
+}
|