- Add "free" relations to CAT

hernanponcedeleon · Feb 26, 2024 · 4e00737 · 4e00737
1 parent bf457e3
commit 4e00737
Show file tree

Hide file tree

Showing 6 changed files with 36 additions and 0 deletions.
diff --git a/dartagnan/src/main/antlr4/Cat.g4 b/dartagnan/src/main/antlr4/Cat.g4
@@ -49,6 +49,7 @@ expression
     |   FENCEREL LPAR e = expression RPAR                               # exprFencerel
     |   LPAR e = expression RPAR                                        # expr
     |   n = NAME                                                        # exprBasic
+    |   call = FREE LPAR RPAR                                           # exprFree
     ;
 
 LET     :   'let';
@@ -81,6 +82,7 @@ RBRAC   :   ']';
 FENCEREL    :   'fencerel';
 DOMAIN      :   'domain';
 RANGE       :   'range';
+FREE        :   'free';
 
 FLAG       :   'flag';
 

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java
@@ -153,6 +153,14 @@ public Void visitDefinition(Definition def) {
             return null;
         }
 
+        @Override
+        public Void visitFree(Free def) {
+            final Relation rel = def.getDefinedRelation();
+            EncodingContext.EdgeEncoder edge = context.edge(rel);
+            encodeSets.get(rel).apply((e1, e2) -> enc.add(bmgr.implication(edge.encode(e1, e2), execution(e1, e2))));
+            return null;
+        }
+
         @Override
         public Void visitUnion(Union union) {
             final Relation rel = union.getDefinedRelation();

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java
@@ -143,6 +143,11 @@ public Object visitExpr(ExprContext ctx) {
         return ctx.e.accept(this);
     }
 
+    @Override
+    public Object visitExprFree(ExprFreeContext ctx) {
+        return addDefinition(new Free(wmm.newRelation()));
+    }
+
     @Override
     public Object visitExprBasic(ExprBasicContext ctx) {
         String name = ctx.n.getText();

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java
@@ -90,6 +90,7 @@ default T visitConstraint(Constraint constraint) {
 
         // Base
         default T visitUndefined(Definition.Undefined def) { return visitDefinition(def); }
+        default T visitFree(Free def) { return visitDefinition(def); }
         default T visitEmpty(Empty def) { return visitDefinition(def); }
         default T visitProgramOrder(ProgramOrder po) { return visitDefinition(po); }
         default T visitExternal(External ext) { return visitDefinition(ext); }

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java
@@ -442,6 +442,21 @@ public Knowledge visitDefinition(Definition def) {
                     : new Knowledge(new EventGraph(), new EventGraph());
         }
 
+        @Override
+        public Knowledge visitFree(Free def) {
+            final List<Event> visibleEvents = program.getThreadEventsWithAllTags(VISIBLE);
+            EventGraph must = new EventGraph();
+            EventGraph may = new EventGraph();
+
+            for (Event e1 : visibleEvents) {
+                for (Event e2 : visibleEvents) {
+                    may.add(e1, e2);
+                }
+            }
+
+            return new Knowledge(may, enableMustSets ? must : EventGraph.empty());
+        }
+
         @Override
         public Knowledge visitProduct(CartesianProduct prod) {
             final Filter domain = prod.getFirstFilter();

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java
@@ -61,6 +61,11 @@ public ForceEncodeAxiom visitForceEncodeAxiom(ForceEncodeAxiom forceEncode) {
         return new ForceEncodeAxiom(forceEncode.getRelation(), forceEncode.isNegated(), forceEncode.isFlagged());
     }
 
+    @Override
+    public Constraint visitFree(Free def) {
+        return new Free(translate(def.getDefinedRelation()));
+    }
+
     @Override
     public Union visitUnion(Union def) {
         return new Union(translate(def.getDefinedRelation()), translate(def.getOperands()));