Fixed a bug in handling of null values in the type checker (#797)

* Fixed a bug in handling of null values in the type checker

* removed the foreign function from two phase commit tutorial example

* Updating tutorial import names

---------

Co-authored-by: Christine Zhou <[email protected]>

Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs

@@ -820,7 +820,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function
                                           && !PrimitiveType.Null.IsSameTypeAs(assignStmt.Value.Type)
                                           && !PrimitiveType.Any.IsSameTypeAs(assignStmt.Location.Type);
                     WriteLValue(context, output, assignStmt.Location);
-                    context.Write(output, $" = ({GetCSharpType(assignStmt.Location.Type)})(");
+                    context.Write(output, $" = ({GetCSharpType(assignStmt.Location.Type, true)})(");
                     if (needCtorAdapter)
                     {
                         context.Write(output, $"new {GetCSharpType(assignStmt.Location.Type)}(");

Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NullLiteralExpr.cs

@@ -12,6 +12,6 @@ public NullLiteralExpr(ParserRuleContext sourceLocation)
 
         public ParserRuleContext SourceLocation { get; }
 
-        public PLanguageType Type { get; } = PrimitiveType.Any;
+        public PLanguageType Type { get; } = PrimitiveType.Null;
     }
 }

Tst/RegressionTests/Feature4DataTypes/StaticError/nullComparison/nullType.p

@@ -0,0 +1,10 @@
+machine Main {
+    start state Init {
+      entry {
+        var x: int;
+        if(x == null) {
+
+        }
+      }
+    }
+  }

Tst/RegressionTests/Feature4DataTypes/StaticError/nullTypeAssign/nullType.p

@@ -0,0 +1,8 @@
+machine Main {
+    start state Init {
+      entry {
+        var x: int;
+        x = null to int;
+      }
+    }
+  }

Tutorial/2_TwoPhaseCommit/PTst/Client.p

@@ -55,9 +55,10 @@ machine Client {
   }
 }
 
-/*  This is an external function (implemented in C#) to randomly choose transaction values
-In P, function declarations without body are considered as foreign functions. */
-fun ChooseRandomTransaction(uniqueId: int): tTrans;
+fun ChooseRandomTransaction(uniqueId: int): tTrans {
+  return (key = format("{0}", choose(10)), val = choose(10), transId = uniqueId);
+}
+
 
 // two phase commit client module
 module TwoPCClient = { Client };

Tutorial/PriorityQueue/PForeign/ClientFunctions.cs

@@ -1,5 +1,5 @@
 using System.Collections;
-using PChecker.PRuntime.Values;
+using PChecker.Runtime.Values;
 
 namespace PImplementation
 {
@@ -9,7 +9,7 @@ namespace PImplementation
      */
     partial class Client
     {
-        public static tPriorityQueue AddIntToQueue(tPriorityQueue queue, IPrtValue elem, PrtInt priority)
+        public static tPriorityQueue AddIntToQueue(tPriorityQueue queue, IPValue elem, PInt priority)
         {
             queue.Add(new ElementWithPriority(elem, priority));
             return queue;

Tutorial/PriorityQueue/PForeign/PriorityQueue.cs

@@ -4,9 +4,9 @@
 using System.Linq;
 using System.IO;
 using System.Linq.Expressions;
-using PChecker.PRuntime;
-using PChecker.PRuntime.Values;
-using PChecker.PRuntime.Exceptions;
+using PChecker.Runtime;
+using PChecker.Runtime.Values;
+using PChecker.Runtime.Exceptions;
 using System.Threading;
 using System.Threading.Tasks;
 
@@ -21,7 +21,7 @@ Apart from that the implementation of the foreign type can be arbitrary sequenti
 
      If you want to pretty print the foreign type value, you can also override the ToString() function in their implementation.
      */
-    public class tPriorityQueue : IPrtValue
+    public class tPriorityQueue : IPValue
     {
         // naive implementation of the priority queue as a list of elements with priority
         private List<ElementWithPriority> elements = new List<ElementWithPriority>();
@@ -39,14 +39,14 @@ public void Delete(ElementWithPriority elem)
         }
 
         // priority remove
-        public IPrtValue PriorityRemove()
+        public IPValue PriorityRemove()
         {
             var removeElem = elements.OrderBy(el => el.Priority).First();
             elements.Remove(removeElem);
             return removeElem.Element;
         }
 
-        public bool Equals(IPrtValue other)
+        public bool Equals(IPValue other)
         {
             if (other is tPriorityQueue || other != null)
             {
@@ -58,7 +58,7 @@ public bool Equals(IPrtValue other)
             }
         }
 
-        public IPrtValue Clone()
+        public IPValue Clone()
         {
             var cloned = new tPriorityQueue();
             foreach (var elem in elements)
@@ -73,18 +73,18 @@ public int Size()
             return elements.Count;
         }
 
-        public IPrtValue GetElementAt(int index)
+        public IPValue GetElementAt(int index)
         {
             return elements.ElementAt(index).Element;
         }
     }
 
     public class ElementWithPriority
     {
-        public IPrtValue Element { get; }
+        public IPValue Element { get; }
         public int Priority { get;  }
 
-        public ElementWithPriority(IPrtValue elem, int priority)
+        public ElementWithPriority(IPValue elem, int priority)
         {
             Element = elem;
             Priority = priority;

Tutorial/PriorityQueue/PForeign/PriorityQueueFunctions.cs

@@ -7,9 +7,10 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.IO;
-using PChecker.PRuntime;
-using PChecker.PRuntime.Values;
-using PChecker.PRuntime.Exceptions;
+using PChecker.Runtime;
+using PChecker.Runtime.Values;
+using PChecker.Runtime.Exceptions;
+using PChecker.Runtime.StateMachines;
 using System.Threading;
 using System.Threading.Tasks;
 
@@ -21,39 +22,39 @@ namespace PImplementation
   // Also, all global foreign functions must be declared static!
   public static partial class GlobalFunctions
   {
-      public static tPriorityQueue CreatePriorityQueue(PMachine machine)
+      public static tPriorityQueue CreatePriorityQueue(StateMachine machine)
       {
           // use these log statements if you want logs in the foreign code to show up in the error trace.
           machine.LogLine("Creating Priority Queue!");
           return new tPriorityQueue();
       }
-      public static tPriorityQueue AddElement(tPriorityQueue queue, IPrtValue elem, PrtInt priority, PMachine machine)
+      public static tPriorityQueue AddElement(tPriorityQueue queue, IPValue elem, PInt priority, StateMachine machine)
       {
           queue.Add(new ElementWithPriority(elem, priority));
           machine.LogLine("Adding Element in the Priority Queue!");
           return queue;
       }
 
-      public static PrtNamedTuple RemoveElement(tPriorityQueue queue, PMachine machine)
+      public static PNamedTuple RemoveElement(tPriorityQueue queue, StateMachine machine)
       {
           var element = queue.PriorityRemove();
-          var retVal = new PrtNamedTuple(new string[] { "element", "queue" }, new IPrtValue[] { element, queue });
+          var retVal = new PNamedTuple(new string[] { "element", "queue" }, new IPValue[] { element, queue });
           return retVal;
       }
 
-      public static PrtInt CountElement(tPriorityQueue queue, PMachine machine)
+      public static PInt CountElement(tPriorityQueue queue, StateMachine machine)
       {
           return queue.Size();
       }
 
       /*
        * Modeling Nondeterminism or Randomness in Foreign Functions
        */
-      public static IPrtValue ChooseElement(tPriorityQueue queue, PMachine machine)
+      public static IPValue ChooseElement(tPriorityQueue queue, StateMachine machine)
       {
           // one can write a nondeterministic foreign function using the machine.*Random functions.
           // all machine.TryRandom*() functions are controlled by the P checker during exploration.
-          var index = machine.TryRandomInt(queue.Size());
+          var index = (PInt)machine.TryRandom((PInt)queue.Size());
           machine.LogLine("Choosing element at location: " + index);
           return queue.GetElementAt(index);
       }