add support for foreign functions with contracts and update one tutor…

…ial to include an example
p-org · Oct 30, 2024 · 4d41085 · 4d41085
1 parent dd47b1e
commit 4d41085
Show file tree

Hide file tree

Showing 7 changed files with 67 additions and 4 deletions.
diff --git a/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Uclid5/Uclid5CodeGenerator.cs
@@ -1121,7 +1121,17 @@ private void GenerateGlobalProcedures(IEnumerable<Function> functions, List<Inva
 
             if (!f.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
             {
-                EmitLine($"\treturns ({BuiltinPrefix}Return: {TypeToString(f.Signature.ReturnType)})");
+                var retName = f.ReturnVariable is null ? $"{BuiltinPrefix}Return" :  $"{LocalPrefix}{f.ReturnVariable.Name}";
+                EmitLine($"\treturns ({retName}: {TypeToString(f.Signature.ReturnType)})");
+            }
+
+            foreach (var req in f.Requires)
+            {
+                EmitLine($"requires {ExprToString(req)};");
+            }
+            foreach (var ensure in f.Ensures)
+            {
+                EmitLine($"ensures {ExprToString(ensure)};");
             }
 
             EmitLine("{");

diff --git a/Src/PCompiler/CompilerCore/CompilerConfiguration.cs b/Src/PCompiler/CompilerCore/CompilerConfiguration.cs
@@ -24,7 +24,7 @@ public CompilerConfiguration()
             Backend = null;
             ProjectDependencies = new List<string>();
             Debug = false;
-            Timeout = 60;
+            Timeout = 600;
             HandlesAll = true;
             CheckOnly = null;
             Parallelism = Math.Max(Environment.ProcessorCount / 2, 1);

diff --git a/Src/PCompiler/CompilerCore/Parser/PLexer.g4 b/Src/PCompiler/CompilerCore/Parser/PLexer.g4
@@ -76,6 +76,8 @@ USING      : 'using';
 LEMMA      : 'Lemma';
 THEOREM    : 'Theorem';
 EXCEPT     : 'except';
+REQUIRES   : 'requires';
+ENSURES    : 'ensures';
 
 // module-system-specific keywords
 

diff --git a/Src/PCompiler/CompilerCore/Parser/PParser.g4 b/Src/PCompiler/CompilerCore/Parser/PParser.g4
@@ -118,6 +118,7 @@ varDecl : VAR idenList COLON type SEMI ;
 
 funDecl : FUN name=iden LPAREN funParamList? RPAREN (COLON type)? (CREATES interfaces+=iden)? SEMI # ForeignFunDecl
         | FUN name=iden LPAREN funParamList? RPAREN (COLON type)? functionBody # PFunDecl
+        | FUN name=iden LPAREN funParamList? RPAREN (RETURN LPAREN funParam RPAREN SEMI)? (REQUIRES requires+=expr SEMI)* (ENSURES ensures+=expr SEMI)* # ForeignFunDecl
         ;
 
 pureDecl : PURE name=iden LPAREN funParamList? RPAREN COLON type (ASSIGN body=expr)? SEMI ;

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs
@@ -23,6 +23,8 @@ public class Function : IPDecl, IHasScope
         private readonly HashSet<Function> callees = new HashSet<Function>();
         private readonly HashSet<Function> callers = new HashSet<Function>();
         private readonly List<Variable> localVariables = new List<Variable>();
+        private readonly List<IPExpr> requireExprs = new List<IPExpr>();
+        private readonly List<IPExpr> ensureExprs = new List<IPExpr>();
         private readonly List<Interface> createsInterfaces = new List<Interface>();
 
         public Function(string name, ParserRuleContext sourceNode)
@@ -57,6 +59,9 @@ public Function(ParserRuleContext sourceNode) : this("", sourceNode)
         public Function ParentFunction { get; set; }
         public FunctionSignature Signature { get; } = new FunctionSignature();
         public IEnumerable<Variable> LocalVariables => localVariables;
+        public Variable ReturnVariable { get; set; }
+        public IEnumerable<IPExpr> Requires => requireExprs;
+        public IEnumerable<IPExpr> Ensures => ensureExprs;
         public IEnumerable<Interface> CreatesInterfaces => createsInterfaces;
         public FunctionRole Role { get; set; }
 
@@ -70,7 +75,15 @@ public void AddLocalVariable(Variable local)
         {
             localVariables.Add(local);
         }
-
+        public void AddRequire(IPExpr expr)
+        {
+            requireExprs.Add(expr);
+        }
+        public void AddEnsure(IPExpr expr)
+        {
+            ensureExprs.Add(expr);
+        }
+
         public void RemoveLocalVariable(Variable local)
         {
             localVariables.Remove(local);

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs
@@ -832,6 +832,40 @@ public override object VisitForeignFunDecl(PParser.ForeignFunDeclContext context
                 else
                     throw Handler.MissingDeclaration(createdInterface, "interface", createdInterface.GetText());
             }
+
+
+            var temporaryFunction = new Function(fun.Name, context);
+            temporaryFunction.Scope = fun.Scope.MakeChildScope();
+
+            // (RETURN LPAREN funParam RPAREN SEMI)?
+            if (context.funParam() != null)
+            {
+                Variable p = (Variable)Visit(context.funParam());
+                // Add the return variable to the scope so that contracts can refer to it 
+                var ret = temporaryFunction.Scope.Put(p.Name, p.SourceLocation, VariableRole.Param);
+                ret.Type = p.Type;
+                nodesToDeclarations.Put(p.SourceLocation, ret);
+                temporaryFunction.Signature.Parameters.Add(ret);
+
+                fun.ReturnVariable = ret;
+                // update the return type to match
+                fun.Signature.ReturnType = fun.ReturnVariable.Type;
+            }
+
+            var exprVisitor = new ExprVisitor(temporaryFunction, Handler);
+
+            // (REQUIRES requires+=expr SEMI)*
+            foreach (var req in context._requires)
+            {
+                fun.AddRequire(exprVisitor.Visit(req));
+            }
+
+            // (ENSURES ensures+=expr SEMI)*
+            foreach (var ensure in context._ensures)
+            {
+                fun.AddEnsure(exprVisitor.Visit(ensure));
+            }
+
             return fun;
         }
 

diff --git a/Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p b/Tutorial/6_TwoPhaseCommitVerification/KeyValue/PSrc/System.p
@@ -33,6 +33,9 @@ event eReadReq  : tReadReq;
 event eReadResp : tReadResp;
 
 fun RandomInt(): int;
+fun RandomParticipant(s: set[machine]) 
+    return (x: machine);
+    ensures x in s;
 
 machine Client {
     start state Loop {
@@ -65,7 +68,7 @@ machine Coordinator
     start state Serving {
         on eReadReq do (req: tReadReq) {
             var p: machine;
-            assume (p in participants());
+            p = RandomParticipant(participants());
             send p, eReadReq, req;
         }