diff --git a/Equivalent mutations/BST.java b/Equivalent mutations/BST.java
new file mode 100644
index 0000000000000000000000000000000000000000..b87578941bdbf042c492ed1e31d32d30f428ea6d
--- /dev/null
+++ b/Equivalent mutations/BST.java
@@ -0,0 +1,126 @@
+// http://www.sanfoundry.com/csharp-program-binary-search-tree-linked-list/
+
+/*
+ * C# Program to Implement Binary Search Tree using Linked List
+ */
+
+class Node
+{
+ public int item;
+ public Node leftc;
+ public Node rightc;
+
+ public void display()
+ {
+ System.out.print("[");
+ System.out.print(this.item);
+ System.out.print("]");
+ }
+}
+
+class Tree
+{
+ public Node root;
+
+ public Tree()
+ {
+ this.root = null;
+ }
+ public Node ReturnRoot()
+ {
+ return this.root;
+ }
+ public void Insert(int id)
+ {
+ Node newNode = new Node();
+ newNode.item = id;
+ if (this.root == null)
+ this.root = newNode;
+ else
+ {
+ Node current = this.root;
+ Node parent;
+
+ while (true)
+ {
+ parent = current;
+ if (id < current.item)
+ {
+ current = current.leftc;
+ if (current == null)
+ {
+ parent.leftc = newNode;
+ return;
+ }
+ }
+ else
+ {
+ current = current.rightc;
+ if (current == null)
+ {
+ parent.rightc = newNode;
+ return;
+ }
+ }
+ }
+ }
+ }
+ public void Preorder(Node root1)
+ {
+ if (root1 != null)
+ {
+ System.out.print(root1.item + " ");
+ Preorder(root1.leftc);
+ Preorder(root1.rightc);
+ }
+ }
+ public void Inorder(Node root2)
+ {
+ if (root2 != null)
+ {
+ Inorder(root2.leftc);
+ System.out.print(root2.item + " ");
+ Inorder(root2.rightc);
+ }
+ }
+ public void Postorder(Node root3)
+ {
+ if (root3 != null)
+ {
+ Postorder(root3.leftc);
+ Postorder(root3.rightc);
+ System.out.print(root3.item + " ");
+ }
+ }
+}
+
+class Program
+{
+ static void main(String[] args)
+ {
+ Tree theTree = new Tree();
+ theTree.Insert(20);
+ theTree.Insert(25);
+ theTree.Insert(45);
+ theTree.Insert(15);
+ theTree.Insert(67);
+ theTree.Insert(43);
+ theTree.Insert(80);
+ theTree.Insert(33);
+ theTree.Insert(67);
+ theTree.Insert(99);
+ theTree.Insert(91);
+ System.out.println("Inorder Traversal : ");
+ theTree.Inorder(theTree.ReturnRoot());
+ System.out.println(" ");
+ System.out.println();
+ System.out.println("Preorder Traversal : ");
+ theTree.Preorder(theTree.ReturnRoot());
+ System.out.println(" ");
+ System.out.println();
+ System.out.println("Postorder Traversal : ");
+ theTree.Postorder(theTree.ReturnRoot());
+ System.out.println(" ");
+ System.in.read();
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Fibonacci.java b/Equivalent mutations/Fibonacci.java
new file mode 100644
index 0000000000000000000000000000000000000000..c8a9a179e02052462280fc1d88115f861e2c22ad
--- /dev/null
+++ b/Equivalent mutations/Fibonacci.java
@@ -0,0 +1,26 @@
+// http://www.sanfoundry.com/csharp-program-generate-fibonocci-series/
+
+/*
+ * C# Program to Generate Fibonacci Series
+ */
+
+class Program
+{
+ static void main(String[] args)
+ {
+ int i, count, f1 = 0, f2 = 1, f3 = 0;
+ System.out.print("Enter the Limit : ");
+ count = System.in.read();
+ System.out.println(f1);
+ System.out.println(f2);
+ for (i = 0; i <= count; i++)
+ {
+ f3 = f1 + f2;
+ System.out.println(f3);
+ f1 = f2;
+ f2 = f3;
+ }
+ System.in.read();
+
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Mutants/BST_no_parent.java b/Equivalent mutations/Mutants/BST_no_parent.java
new file mode 100644
index 0000000000000000000000000000000000000000..e5d8c9e568de67abf7709eb06920ef73e5b7318b
--- /dev/null
+++ b/Equivalent mutations/Mutants/BST_no_parent.java
@@ -0,0 +1,124 @@
+// http://www.sanfoundry.com/csharp-program-binary-search-tree-linked-list/
+
+/*
+ * C# Program to Implement Binary Search Tree using Linked List
+ */
+
+class Node
+{
+ public int item;
+ public Node leftc;
+ public Node rightc;
+
+ public void display()
+ {
+ System.out.print("[");
+ System.out.print(this.item);
+ System.out.print("]");
+ }
+}
+
+class Tree
+{
+ public Node root;
+
+ public Tree()
+ {
+ this.root = null;
+ }
+ public Node ReturnRoot()
+ {
+ return this.root;
+ }
+ public void Insert(int id)
+ {
+ Node newNode = new Node();
+ newNode.item = id;
+ if (this.root == null)
+ this.root = newNode;
+ else
+ {
+ Node current = this.root;
+ while (true)
+ {
+ if (id < current.item)
+ {
+ if (current.leftc == null)
+ {
+ current.leftc = newNode;
+ return;
+ }
+ current = current.leftc;
+ }
+ else
+ {
+ if (current.rightc == null)
+ {
+ current.rightc = newNode;
+ return;
+ }
+ current = current.rightc;
+ }
+ }
+ }
+ }
+ }
+ public void Preorder(Node root1)
+ {
+ if (root1 != null)
+ {
+ System.out.print(root1.item + " ");
+ Preorder(root1.leftc);
+ Preorder(root1.rightc);
+ }
+ }
+ public void Inorder(Node root2)
+ {
+ if (root2 != null)
+ {
+ Inorder(root2.leftc);
+ System.out.print(root2.item + " ");
+ Inorder(root2.rightc);
+ }
+ }
+ public void Postorder(Node root3)
+ {
+ if (root3 != null)
+ {
+ Postorder(root3.leftc);
+ Postorder(root3.rightc);
+ System.out.print(root3.item + " ");
+ }
+ }
+}
+
+class Program
+{
+ static void main(String[] args)
+ {
+ Tree theTree = new Tree();
+ theTree.Insert(20);
+ theTree.Insert(25);
+ theTree.Insert(45);
+ theTree.Insert(15);
+ theTree.Insert(67);
+ theTree.Insert(43);
+ theTree.Insert(80);
+ theTree.Insert(33);
+ theTree.Insert(67);
+ theTree.Insert(99);
+ theTree.Insert(91);
+ System.out.println("Inorder Traversal : ");
+ theTree.Inorder(theTree.ReturnRoot());
+ System.out.println(" ");
+ System.out.println();
+ System.out.println("Preorder Traversal : ");
+ theTree.Preorder(theTree.ReturnRoot());
+ System.out.println(" ");
+ System.out.println();
+ System.out.println("Postorder Traversal : ");
+ theTree.Postorder(theTree.ReturnRoot());
+ System.out.println(" ");
+ System.in.read();
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Mutants/Fibonacci_no_extra_prints.java b/Equivalent mutations/Mutants/Fibonacci_no_extra_prints.java
new file mode 100644
index 0000000000000000000000000000000000000000..e45c9c68f43cd54b05b24d83afc9054637219906
--- /dev/null
+++ b/Equivalent mutations/Mutants/Fibonacci_no_extra_prints.java
@@ -0,0 +1,24 @@
+// http://www.sanfoundry.com/csharp-program-generate-fibonocci-series/
+
+/*
+ * C# Program to Generate Fibonacci Series
+ */
+
+class Program
+{
+ static void main(String[] args)
+ {
+ int i, count, f1 = 0, f2 = 1, f3 = 0;
+ System.out.print("Enter the Limit : ");
+ count = System.in.read();
+ for (i = 0; i <= count + 2; i++)
+ {
+ f3 = f1 + f2;
+ System.out.println(f1);
+ f1 = f2;
+ f2 = f3;
+ }
+ System.in.read();
+
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Mutants/Stack_bool_is_result.java b/Equivalent mutations/Mutants/Stack_bool_is_result.java
new file mode 100644
index 0000000000000000000000000000000000000000..d40fff2bc3d95e74f98e8919b98dc2fb03827979
--- /dev/null
+++ b/Equivalent mutations/Mutants/Stack_bool_is_result.java
@@ -0,0 +1,126 @@
+// http://www.sanfoundry.com/csharp-program-stack-push-pop/
+
+/*
+ * C# Program to Implement Stack with Push and Pop operations
+ */
+
+class Program
+{
+ static void main(String[] args)
+ {
+ stack st = new stack();
+ while (true)
+ {
+ System.out.println("\nStack MENU(size -- 10)");
+ System.out.println("1. Add an element");
+ System.out.println("2. See the Top element.");
+ System.out.println("3. Remove top element.");
+ System.out.println("4. Display stack elements.");
+ System.out.println("5. Exit");
+ System.out.print("Select your choice: ");
+ int choice = System.in.read();
+ switch (choice)
+ {
+ case 1:
+ System.out.println("Enter an Element : ");
+ st.Push(System.in.read());
+ break;
+
+ case 2: System.out.printf("Top element is: {0}", st.Peek());
+ break;
+
+ case 3: System.out.printf("Element removed: {0}", st.Pop());
+ break;
+
+ case 4: st.Display();
+ break;
+
+ case 5: System.exit(1);
+ break;
+ }
+ System.in.read();
+ }
+ }
+ }
+
+ interface StackADT
+ {
+ boolean isEmpty();
+ void Push(Object element);
+ Object Pop();
+ Object Peek();
+ void Display();
+ }
+
+ class stack implements StackADT
+ {
+ public int StackSize;
+ public int top;
+ Object[] item;
+
+ public stack()
+ {
+ this.StackSize = 10;
+ this.item = new Object[this.StackSize];
+ this.top = -1;
+ }
+ public stack(int capacity)
+ {
+ this.StackSize = capacity;
+ this.item = new Object[this.StackSize];
+ this.top = -1;
+ }
+ public boolean isEmpty()
+ {
+ return this.top == -1;
+ }
+ public void Push(Object element)
+ {
+ if (this.top == (this.StackSize - 1))
+ {
+ System.out.println("Stack is full!");
+ }
+
+ else
+ {
+
+ this.item[++this.top] = element;
+ System.out.println("Item pushed successfully!");
+ }
+ }
+ public Object Pop()
+ {
+ if (isEmpty())
+ {
+ System.out.println("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+
+ return this.item[this.top--];
+ }
+ }
+ public Object Peek()
+ {
+ if (isEmpty())
+ {
+ System.out.println("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+ return this.item[this.top];
+ }
+ }
+
+
+ public void Display()
+ {
+ for (int i = this.top; i > -1; i--)
+ {
+
+ System.out.printf("Item {0}: {1}", (i + 1), this.item[i]);
+ }
+ }
+}
diff --git a/Equivalent mutations/Mutants/Stack_constructor_duplication.java b/Equivalent mutations/Mutants/Stack_constructor_duplication.java
new file mode 100644
index 0000000000000000000000000000000000000000..151eb58e6e9ef490e13c9e00f478151c0317cbd1
--- /dev/null
+++ b/Equivalent mutations/Mutants/Stack_constructor_duplication.java
@@ -0,0 +1,126 @@
+// http://www.sanfoundry.com/csharp-program-stack-push-pop/
+
+/*
+ * C# Program to Implement Stack with Push and Pop operations
+ */
+
+class Program
+{
+ static void main(String[] args)
+ {
+ stack st = new stack();
+ while (true)
+ {
+ System.out.println("\nStack MENU(size -- 10)");
+ System.out.println("1. Add an element");
+ System.out.println("2. See the Top element.");
+ System.out.println("3. Remove top element.");
+ System.out.println("4. Display stack elements.");
+ System.out.println("5. Exit");
+ System.out.print("Select your choice: ");
+ int choice = System.in.read();
+ switch (choice)
+ {
+ case 1:
+ System.out.println("Enter an Element : ");
+ st.Push(System.in.read());
+ break;
+
+ case 2: System.out.printf("Top element is: {0}", st.Peek());
+ break;
+
+ case 3: System.out.printf("Element removed: {0}", st.Pop());
+ break;
+
+ case 4: st.Display();
+ break;
+
+ case 5: System.exit(1);
+ break;
+ }
+ System.in.read();
+ }
+ }
+ }
+
+ interface StackADT
+ {
+ boolean isEmpty();
+ void Push(Object element);
+ Object Pop();
+ Object Peek();
+ void Display();
+ }
+
+ class stack implements StackADT
+ {
+ public int StackSize;
+ public int top;
+ Object[] item;
+
+ public stack()
+ {
+ this(10);
+ }
+ public stack(int capacity)
+ {
+ this.StackSize = capacity;
+ this.item = new Object[this.StackSize];
+ this.top = -1;
+ }
+ public boolean isEmpty()
+ {
+ if (this.top == -1) return true;
+
+ return false;
+ }
+ public void Push(Object element)
+ {
+ if (this.top == (this.StackSize - 1))
+ {
+ System.out.println("Stack is full!");
+ }
+
+ else
+ {
+
+ this.item[++this.top] = element;
+ System.out.println("Item pushed successfully!");
+ }
+ }
+ public Object Pop()
+ {
+ if (isEmpty())
+ {
+ System.out.println("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+
+ return this.item[this.top--];
+ }
+ }
+ public Object Peek()
+ {
+ if (isEmpty())
+ {
+ System.out.println("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+ return this.item[this.top];
+ }
+ }
+
+
+ public void Display()
+ {
+ for (int i = this.top; i > -1; i--)
+ {
+
+ System.out.printf("Item {0}: {1}", (i + 1), this.item[i]);
+ }
+ }
+}
diff --git a/Equivalent mutations/Mutants/Stack_useless_property.java b/Equivalent mutations/Mutants/Stack_useless_property.java
new file mode 100644
index 0000000000000000000000000000000000000000..9a37ee62a5542d45073642fc4f6a8fcdb4983982
--- /dev/null
+++ b/Equivalent mutations/Mutants/Stack_useless_property.java
@@ -0,0 +1,126 @@
+// http://www.sanfoundry.com/csharp-program-stack-push-pop/
+
+/*
+ * C# Program to Implement Stack with Push and Pop operations
+ */
+
+class Program
+{
+ static void main(String[] args)
+ {
+ stack st = new stack();
+ while (true)
+ {
+ System.out.println("\nStack MENU(size -- 10)");
+ System.out.println("1. Add an element");
+ System.out.println("2. See the Top element.");
+ System.out.println("3. Remove top element.");
+ System.out.println("4. Display stack elements.");
+ System.out.println("5. Exit");
+ System.out.print("Select your choice: ");
+ int choice = System.in.read();
+ switch (choice)
+ {
+ case 1:
+ System.out.println("Enter an Element : ");
+ st.Push(System.in.read());
+ break;
+
+ case 2: System.out.printf("Top element is: {0}", st.Peek());
+ break;
+
+ case 3: System.out.printf("Element removed: {0}", st.Pop());
+ break;
+
+ case 4: st.Display();
+ break;
+
+ case 5: System.exit(1);
+ break;
+ }
+ System.in.read();
+ }
+ }
+ }
+
+ interface StackADT
+ {
+ boolean isEmpty();
+ void Push(Object element);
+ Object Pop();
+ Object Peek();
+ void Display();
+ }
+
+ class stack implements StackADT
+ {
+ public int StackSize;
+ public int top;
+ Object[] item;
+
+ public stack()
+ {
+ this.item = new Object[10];
+ this.top = -1;
+ }
+ public stack(int capacity)
+ {
+ this.item = new Object[capacity];
+ this.top = -1;
+ }
+ public boolean isEmpty()
+ {
+ if (top == -1) return true;
+
+ return false;
+ }
+ public void Push(Object element)
+ {
+ if (this.top == (this.StackSize - 1))
+ {
+ System.out.println("Stack is full!");
+ }
+
+ else
+ {
+
+ this.item[++this.top] = element;
+ System.out.println("Item pushed successfully!");
+ }
+ }
+ public Object Pop()
+ {
+ if (isEmpty())
+ {
+ System.out.println("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+
+ return this.item[this.top--];
+ }
+ }
+ public Object Peek()
+ {
+ if (isEmpty())
+ {
+ System.out.println("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+ return this.item[this.top];
+ }
+ }
+
+
+ public void Display()
+ {
+ for (int i = this.top; i > -1; i--)
+ {
+
+ System.out.printf("Item {0}: {1}", (i + 1), this.item[i]);
+ }
+ }
+}
diff --git a/Equivalent mutations/Stack.java b/Equivalent mutations/Stack.java
new file mode 100644
index 0000000000000000000000000000000000000000..d67d9f1ded8e33528f4dab236afff195b9e7fd59
--- /dev/null
+++ b/Equivalent mutations/Stack.java
@@ -0,0 +1,128 @@
+// http://www.sanfoundry.com/csharp-program-stack-push-pop/
+
+/*
+ * C# Program to Implement Stack with Push and Pop operations
+ */
+
+class Program
+{
+ static void main(String[] args)
+ {
+ stack st = new stack();
+ while (true)
+ {
+ System.out.println("\nStack MENU(size -- 10)");
+ System.out.println("1. Add an element");
+ System.out.println("2. See the Top element.");
+ System.out.println("3. Remove top element.");
+ System.out.println("4. Display stack elements.");
+ System.out.println("5. Exit");
+ System.out.print("Select your choice: ");
+ int choice = System.in.read();
+ switch (choice)
+ {
+ case 1:
+ System.out.println("Enter an Element : ");
+ st.Push(System.in.read());
+ break;
+
+ case 2: System.out.printf("Top element is: {0}", st.Peek());
+ break;
+
+ case 3: System.out.printf("Element removed: {0}", st.Pop());
+ break;
+
+ case 4: st.Display();
+ break;
+
+ case 5: System.exit(1);
+ break;
+ }
+ System.in.read();
+ }
+ }
+ }
+
+ interface StackADT
+ {
+ boolean isEmpty();
+ void Push(Object element);
+ Object Pop();
+ Object Peek();
+ void Display();
+ }
+
+ class stack implements StackADT
+ {
+ public int StackSize;
+ public int top;
+ Object[] item;
+
+ public stack()
+ {
+ this.StackSize = 10;
+ this.item = new Object[this.StackSize];
+ this.top = -1;
+ }
+ public stack(int capacity)
+ {
+ this.StackSize = capacity;
+ this.item = new Object[this.StackSize];
+ this.top = -1;
+ }
+ public boolean isEmpty()
+ {
+ if (this.top == -1) return true;
+
+ return false;
+ }
+ public void Push(Object element)
+ {
+ if (this.top == (this.StackSize - 1))
+ {
+ System.out.println("Stack is full!");
+ }
+
+ else
+ {
+
+ this.item[++this.top] = element;
+ System.out.println("Item pushed successfully!");
+ }
+ }
+ public Object Pop()
+ {
+ if (isEmpty())
+ {
+ System.out.println("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+
+ return this.item[this.top--];
+ }
+ }
+ public Object Peek()
+ {
+ if (isEmpty())
+ {
+ System.out.println("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+ return this.item[this.top];
+ }
+ }
+
+
+ public void Display()
+ {
+ for (int i = this.top; i > -1; i--)
+ {
+
+ System.out.printf("Item {0}: {1}", (i + 1), this.item[i]);
+ }
+ }
+}
diff --git a/Equivalent mutations/BST.cs b/Equivalent mutations/original C# code/BST.cs
similarity index 100%
rename from Equivalent mutations/BST.cs
rename to Equivalent mutations/original C# code/BST.cs
diff --git a/Equivalent mutations/Mutants/BST_no_parent.cs b/Equivalent mutations/original C# code/BST_no_parent.cs
similarity index 100%
rename from Equivalent mutations/Mutants/BST_no_parent.cs
rename to Equivalent mutations/original C# code/BST_no_parent.cs
diff --git a/Equivalent mutations/Fibonacci.cs b/Equivalent mutations/original C# code/Fibonacci.cs
similarity index 100%
rename from Equivalent mutations/Fibonacci.cs
rename to Equivalent mutations/original C# code/Fibonacci.cs
diff --git a/Equivalent mutations/Mutants/Fibonacci_no_extra_prints.cs b/Equivalent mutations/original C# code/Fibonacci_no_extra_prints.cs
similarity index 100%
rename from Equivalent mutations/Mutants/Fibonacci_no_extra_prints.cs
rename to Equivalent mutations/original C# code/Fibonacci_no_extra_prints.cs
diff --git a/Equivalent mutations/Heapsort.cs b/Equivalent mutations/original C# code/Heapsort.cs
similarity index 100%
rename from Equivalent mutations/Heapsort.cs
rename to Equivalent mutations/original C# code/Heapsort.cs
diff --git a/Equivalent mutations/Matrix.cs b/Equivalent mutations/original C# code/Matrix.cs
similarity index 100%
rename from Equivalent mutations/Matrix.cs
rename to Equivalent mutations/original C# code/Matrix.cs
diff --git a/Equivalent mutations/Stack.cs b/Equivalent mutations/original C# code/Stack.cs
similarity index 100%
rename from Equivalent mutations/Stack.cs
rename to Equivalent mutations/original C# code/Stack.cs
diff --git a/Equivalent mutations/Mutants/Stack_bool_is_result.cs b/Equivalent mutations/original C# code/Stack_bool_is_result.cs
similarity index 100%
rename from Equivalent mutations/Mutants/Stack_bool_is_result.cs
rename to Equivalent mutations/original C# code/Stack_bool_is_result.cs
diff --git a/Equivalent mutations/Mutants/Stack_constructor_duplication.cs b/Equivalent mutations/original C# code/Stack_constructor_duplication.cs
similarity index 100%
rename from Equivalent mutations/Mutants/Stack_constructor_duplication.cs
rename to Equivalent mutations/original C# code/Stack_constructor_duplication.cs
diff --git a/Equivalent mutations/Mutants/Stack_useless_property.cs b/Equivalent mutations/original C# code/Stack_useless_property.cs
similarity index 100%
rename from Equivalent mutations/Mutants/Stack_useless_property.cs
rename to Equivalent mutations/original C# code/Stack_useless_property.cs
diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index 05c39c01421cdc499f291cfdeaaf9f3376380a95..dbdacb72d3233b8cb40d41277448fe6405e0ccdd 100644
--- a/HelperFunctions.hs
+++ b/HelperFunctions.hs
@@ -40,6 +40,25 @@ getFieldType decls (RefType (ClassRefType t)) (Name (f:fs)) = getFieldType decls
_ -> getDecl t xs
getDecl t _ = error ("fieldType: " ++ show t)
+-- | Gets the type of the class in which the method is defined
+getMethodClassType :: [TypeDecl] -> Ident -> Type
+getMethodClassType decls id = head $ concatMap (flip getMethodTypeFromClassDecl id) decls
+ where
+ getMethodTypeFromClassDecl :: TypeDecl -> Ident -> [Type]
+ getMethodTypeFromClassDecl (ClassTypeDecl (ClassDecl _ className _ _ _ (ClassBody decls))) id = getMethodTypeFromMemberDecls (RefType (ClassRefType (ClassType [(className , [])]))) decls id
+ getMethodTypeFromClassDecl _ _ = []
+
+ getMethodTypeFromMemberDecls :: Type -> [Decl] -> Ident -> [Type]
+ getMethodTypeFromMemberDecls t [] _ = []
+ getMethodTypeFromMemberDecls t (MemberDecl (MethodDecl _ _ _ id' _ _ _) : decls) id = if id' == id then [t] else getMethodTypeFromMemberDecls t decls id
+ getMethodTypeFromMemberDecls t (_ : decls) id = getMethodTypeFromMemberDecls t decls id
+
+-- | Adds the special variables *obj, returnValue and returnValueVar to a type environment, given the id of the method we're looking at
+extendEnv :: TypeEnv -> [TypeDecl] -> Ident -> TypeEnv
+extendEnv env decls methodId = case getMethodType decls methodId of
+ Nothing -> (Name [Ident "*obj"], getMethodClassType decls methodId) : env
+ Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : (Name [Ident "*obj"], getMethodClassType decls methodId) : env
+
-- | Creates a string that that represents the return var name of a method call. This name is extended by a number to indicate the depth of the recursive calls
makeReturnVarName :: Ident -> String
makeReturnVarName (Ident s) = "$" ++ s ++ "$"
diff --git a/Main.hs b/Main.hs
index efe15682c1b7f797dbd7e2bad8078046a5e9d848..76d20b45d7181f66fd1c2478805a8662d8114b0d 100644
--- a/Main.hs
+++ b/Main.hs
@@ -71,9 +71,7 @@ wlpMethod env decls ident = do
let returnType = getMethodType decls ident
-- Add returnValue to the type environment with the correct type
- let env' = case returnType of
- Nothing -> env
- Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : env
+ let env' = extendEnv env decls ident
-- Calculate the wlp. Note that the post condition might depend on the type of the function
let pred = wlpWithEnv decls env' (fromJust' "wlpMethod" $ getMethod decls ident) (getPostCond returnType)
@@ -89,11 +87,7 @@ compareWlps env decls s (path, s') = do
where
compareMethod (ident, e) = case lookup ident s' of
Nothing -> putStrLn ("The method \'" ++ show ident ++ "\' is missing in one of the mutations.") >> return 0 -- print a warning and return 0 errors found
- Just e' -> if unsafeIsTrue (extendEnv env decls ident) (e `imp` e') then return 0 else putStrLn ("error detected in mutation: " ++ path ++ " method: " ++ prettyPrint ident) >> return 1 -- print a message and return 1 error found
- -- Adds returnValue to the type environment with the correct type
- extendEnv env decls ident = case getMethodType decls ident of
- Nothing -> env
- Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : env
+ Just e' -> if unsafeIsTrue (extendEnv env decls ident) decls (e `imp` e') then return 0 else putStrLn ("error detected in mutation: " ++ path ++ " method: " ++ prettyPrint ident) >> return 1 -- print a message and return 1 error found
-- Gets the right post-condition given the type of a method
getPostCond :: Maybe Type -> Exp
@@ -108,7 +102,7 @@ getPostCond t = case parser Language.Java.Parser.exp postCond' of
-- Calculate the wlp (for testing purposes)
calcWlp :: IO ()
calcWlp = do
- source <- readFile (joinPath ["Tests", testFile ++ ".java"])
+ source <- readFile (joinPath ["Equivalent mutations", "BST.java"]) -- sourcePath
let result = parser compilationUnit source
@@ -118,10 +112,5 @@ calcWlp = do
let decls = getDecls compUnit
let methods = if ignoreMainMethod then filter (/= Ident "main") (getMethodIds decls) else getMethodIds decls
let env = getTypeEnv compUnit decls methods
- let printMethodWlp = (\ident e -> putStrLn (prettyPrint ident ++ ":\r\n" ++ prettyPrint e ++ "\r\n" ++ (if unsafeIsTrue (extendEnv env decls ident) e then "WLP evaluates to true" else (if unsafeIsFalse (extendEnv env decls ident) e then "WLP evaluates to false" else "undecidable")) ++ "\r\n"))
- mapM_ (\ident -> wlpMethod env decls ident >>= printMethodWlp ident) methods
- where
- -- Adds returnValue to the type environment with the correct type
- extendEnv env decls ident = case getMethodType decls ident of
- Nothing -> env
- Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : env
\ No newline at end of file
+ let printMethodWlp = (\ident e -> putStrLn (prettyPrint ident ++ ":\r\n" ++ prettyPrint e ++ "\r\n" ++ (if unsafeIsTrue (extendEnv env decls ident) decls e then "WLP evaluates to true" else (if unsafeIsFalse (extendEnv env decls ident) decls e then "WLP evaluates to false" else "undecidable")) ++ "\r\n"))
+ mapM_ (\ident -> wlpMethod env decls ident >>= printMethodWlp ident) methods
\ No newline at end of file
diff --git a/Verifier.hs b/Verifier.hs
index d05c8c561152885816ffe6ecc66491a6f23cbe6f..b9114cdc3a99519b2517dcf6d04ca674458f5db7 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -11,15 +11,15 @@ import Settings
-- | Checks wether the negation is unsatisfiable
-isTrue :: TypeEnv -> Exp -> Z3 Bool
-isTrue env e = isFalse env (PreNot e)
+isTrue :: TypeEnv -> [TypeDecl] -> Exp -> Z3 Bool
+isTrue env decls e = isFalse env decls (PreNot e)
-- | Checks wether the expression is unsatisfiable
-isFalse :: TypeEnv -> Exp -> Z3 Bool
-isFalse env e =
+isFalse :: TypeEnv -> [TypeDecl] -> Exp -> Z3 Bool
+isFalse env decls e =
do
- ast <- foldExp expAssertAlgebra e env
+ ast <- foldExp expAssertAlgebra e env decls
assert ast
result <- check
solverReset
@@ -28,12 +28,12 @@ isFalse env e =
_ -> return False
-- | Unsafe version of isTrue
-unsafeIsTrue :: TypeEnv -> Exp -> Bool
-unsafeIsTrue env = unsafePerformIO . evalZ3 . isTrue env
+unsafeIsTrue :: TypeEnv -> [TypeDecl] -> Exp -> Bool
+unsafeIsTrue env decls = unsafePerformIO . evalZ3 . isTrue env decls
-- | Unsafe version of isFalse
-unsafeIsFalse :: TypeEnv -> Exp -> Bool
-unsafeIsFalse env = unsafePerformIO . evalZ3 . isFalse env
+unsafeIsFalse :: TypeEnv -> [TypeDecl] -> Exp -> Bool
+unsafeIsFalse env decls = unsafePerformIO . evalZ3 . isFalse env decls
stringToBv :: String -> Z3 AST
stringToBv [] = mkIntNum 0 >>= mkInt2bv 8
@@ -45,9 +45,9 @@ stringToBv (c:cs) = do
-- | Defines the convertion from an expression to AST so that Z3 can assert satisfiability
-- This is used to fold expressions generated by the WLP transformer, so not all valid Java expressions need to be handled
-expAssertAlgebra :: ExpAlgebra (TypeEnv -> Z3 AST)
+expAssertAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> Z3 AST)
expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualInstanceCreation, fArrayCreate, fArrayCreateInit, fFieldAccess, fMethodInv, fArrayAccess, fExpName, fPostIncrement, fPostDecrement, fPreIncrement, fPreDecrement, fPrePlus, fPreMinus, fPreBitCompl, fPreNot, fCast, fBinOp, fInstanceOf, fCond, fAssign, fLambda, fMethodRef) where
- fLit lit _ = case lit of
+ fLit lit _ _ = case lit of
Int n -> mkInteger n
Word n -> mkInteger n
Float d -> mkRealNum d
@@ -65,141 +65,141 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
fQualInstanceCreation = undefined
fArrayCreate = error "ArrayCreate"
fArrayCreateInit = undefined
- fFieldAccess fieldAccess _ = case fieldAccess of
+ fFieldAccess fieldAccess _ _ = case fieldAccess of
PrimaryFieldAccess e id -> case e of
InstanceCreation _ t args _ -> undefined
_ -> undefined
SuperFieldAccess id -> mkStringSymbol (prettyPrint (Name [id])) >>= mkIntVar
ClassFieldAccess (Name name) id -> mkStringSymbol (prettyPrint (Name (name ++ [id]))) >>= mkIntVar
- fMethodInv invocation env = case invocation of
- MethodCall (Name [Ident "*length"]) [a, (Lit (Int n))] -> case a of
- ArrayCreate t exps dim -> foldExp expAssertAlgebra (if fromEnum n < length exps then (exps !! fromEnum n) else Lit (Int 0)) env
- ArrayCreateInit t dim arrayInit -> mkInteger 0
- ExpName name -> do
- symbol <- mkStringSymbol ("*length(" ++ prettyPrint name ++ ", " ++ show n ++ ")")
- mkIntVar symbol
- Cond g a1 a2 -> foldExp expAssertAlgebra (Cond g (MethodInv (MethodCall (Name [Ident "*length"]) [a1, (Lit (Int n))])) (MethodInv (MethodCall (Name [Ident "*length"]) [a2, (Lit (Int n))]))) env
- Lit Null -> mkInteger (-1)
- _ -> error ("length of non-array: " ++ prettyPrint a)
- _ -> error (prettyPrint invocation)
- fArrayAccess arrayIndex env = case arrayIndex of
- ArrayIndex (ArrayCreate t _ _) _ -> foldExp expAssertAlgebra (getInitValue t) env
- ArrayIndex (ArrayCreateInit t _ _) _ -> foldExp expAssertAlgebra (getInitValue t) env
- ArrayIndex (ExpName name) i -> do
- symbol <- mkStringSymbol (prettyPrint name ++ "[" ++ show i ++ "]")
- case fmap arrayContentType (lookup name env) of
- Just (PrimType BooleanT) -> mkBoolVar symbol
- Just (PrimType FloatT) -> mkRealVar symbol
- Just (PrimType DoubleT) -> mkRealVar symbol
- _ -> mkIntVar symbol
- ArrayIndex (Cond g a1 a2) i -> foldExp expAssertAlgebra (Cond g (ArrayAccess (ArrayIndex a1 i)) (ArrayAccess (ArrayIndex a2 i))) env
- ArrayIndex e _ -> foldExp expAssertAlgebra e env
- fExpName name env = do
+ fMethodInv invocation env decls = case invocation of
+ MethodCall (Name [Ident "*length"]) [a, (Lit (Int n))] -> case a of
+ ArrayCreate t exps dim -> foldExp expAssertAlgebra (if fromEnum n < length exps then (exps !! fromEnum n) else Lit (Int 0)) env decls
+ ArrayCreateInit t dim arrayInit -> mkInteger 0
+ ExpName name -> do
+ symbol <- mkStringSymbol ("*length(" ++ prettyPrint name ++ ", " ++ show n ++ ")")
+ mkIntVar symbol
+ Cond g a1 a2 -> foldExp expAssertAlgebra (Cond g (MethodInv (MethodCall (Name [Ident "*length"]) [a1, (Lit (Int n))])) (MethodInv (MethodCall (Name [Ident "*length"]) [a2, (Lit (Int n))]))) env decls
+ Lit Null -> mkInteger (-1)
+ _ -> error ("length of non-array: " ++ prettyPrint a)
+ _ -> error (prettyPrint invocation)
+ fArrayAccess arrayIndex env decls = case arrayIndex of
+ ArrayIndex (ArrayCreate t _ _) _ -> foldExp expAssertAlgebra (getInitValue t) env decls
+ ArrayIndex (ArrayCreateInit t _ _) _ -> foldExp expAssertAlgebra (getInitValue t) env decls
+ ArrayIndex (ExpName name) i -> do
+ symbol <- mkStringSymbol (prettyPrint name ++ "[" ++ show i ++ "]")
+ case arrayContentType (lookupType decls env name) of
+ PrimType BooleanT -> mkBoolVar symbol
+ PrimType FloatT -> mkRealVar symbol
+ PrimType DoubleT -> mkRealVar symbol
+ _ -> mkIntVar symbol
+ ArrayIndex (Cond g a1 a2) i -> foldExp expAssertAlgebra (Cond g (ArrayAccess (ArrayIndex a1 i)) (ArrayAccess (ArrayIndex a2 i))) env decls
+ ArrayIndex e _ -> foldExp expAssertAlgebra e env decls
+ fExpName name env decls = do
symbol <- mkStringSymbol (prettyPrint name)
- case lookup name env of
- Just (PrimType BooleanT) -> mkBoolVar symbol
- Just (PrimType FloatT) -> mkRealVar symbol
- Just (PrimType DoubleT) -> mkRealVar symbol
- Just (PrimType IntT) -> mkIntVar symbol
- Just (RefType _) -> mkIntVar symbol
+ case lookupType decls env name of
+ PrimType BooleanT -> mkBoolVar symbol
+ PrimType FloatT -> mkRealVar symbol
+ PrimType DoubleT -> mkRealVar symbol
+ PrimType IntT -> mkIntVar symbol
+ RefType _ -> mkIntVar symbol
-- For now, we assume library methods return ints. Fixing this would require type information of library methods.
t -> if ignoreLibMethods then mkStringSymbol "libMethodCall" >>= mkIntVar else error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
fPostIncrement = undefined
fPostDecrement = undefined
fPreIncrement = undefined
fPreDecrement = undefined
- fPrePlus e env = e env
- fPreMinus e env = do
- ast <- e env
- zero <- mkInteger 0
- mkSub [zero, ast]
+ fPrePlus e env decls = e env decls
+ fPreMinus e env decls = do
+ ast <- e env decls
+ zero <- mkInteger 0
+ mkSub [zero, ast]
fPreBitCompl = undefined
- fPreNot e env = e env >>= mkNot
+ fPreNot e env decls = e env decls >>= mkNot
fCast = undefined
- fBinOp e1 op e2 env = case op of
- Mult -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkMul [ast1, ast2]
- Div -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkDiv ast1 ast2
- Rem -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkRem ast1 ast2
- Add -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkAdd [ast1, ast2]
- Sub -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkSub [ast1, ast2]
- LShift -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkBvshl ast1 ast2
- RShift -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkBvashr ast1 ast2
- RRShift -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkBvlshr ast1 ast2
- LThan -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkLt ast1 ast2
- GThan -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkGt ast1 ast2
- LThanE -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkLe ast1 ast2
- GThanE -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkGe ast1 ast2
- Equal -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkEq ast1 ast2
- NotEq -> do
- ast1 <- e1 env
- ast2 <- e2 env
- eq <- mkEq ast1 ast2
- mkNot eq
- And-> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkAnd [ast1, ast2]
- Or -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkOr [ast1, ast2]
- Xor -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkXor ast1 ast2
- CAnd -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkAnd [ast1, ast2]
- COr -> do
- ast1 <- e1 env
- ast2 <- e2 env
- mkOr [ast1, ast2]
+ fBinOp e1 op e2 env decls = case op of
+ Mult -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkMul [ast1, ast2]
+ Div -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkDiv ast1 ast2
+ Rem -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkRem ast1 ast2
+ Add -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkAdd [ast1, ast2]
+ Sub -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkSub [ast1, ast2]
+ LShift -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkBvshl ast1 ast2
+ RShift -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkBvashr ast1 ast2
+ RRShift -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkBvlshr ast1 ast2
+ LThan -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkLt ast1 ast2
+ GThan -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkGt ast1 ast2
+ LThanE -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkLe ast1 ast2
+ GThanE -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkGe ast1 ast2
+ Equal -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkEq ast1 ast2
+ NotEq -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ eq <- mkEq ast1 ast2
+ mkNot eq
+ And-> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkAnd [ast1, ast2]
+ Or -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkOr [ast1, ast2]
+ Xor -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkXor ast1 ast2
+ CAnd -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkAnd [ast1, ast2]
+ COr -> do
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkOr [ast1, ast2]
fInstanceOf = undefined
- fCond g e1 e2 env = do
- astg <- g env
- ast1 <- e1 env
- ast2 <- e2 env
- mkIte astg ast1 ast2
+ fCond g e1 e2 env decls = do
+ astg <- g env decls
+ ast1 <- e1 env decls
+ ast2 <- e2 env decls
+ mkIte astg ast1 ast2
fAssign = undefined
fLambda = undefined
fMethodRef = undefined
\ No newline at end of file
diff --git a/WLP.hs b/WLP.hs
index 92ebee659b6f83f5ae7fd552171363852ab3f65a..4e13645af212df01f2a82e8e8cd3298bd2f676b0 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -301,7 +301,7 @@ wlp decls = wlpWithEnv decls []
-- | wlp with a given type environment
wlpWithEnv :: [TypeDecl] -> TypeEnv -> Stmt -> Exp -> Exp
-wlpWithEnv decls env = wlp' (Inh id id Nothing env decls [] (Just (Ident "returnValue")) (Just (ExpName (Name [Ident "#obj"]))))
+wlpWithEnv decls env = wlp' (Inh id id Nothing env decls [] (Just (Ident "returnValue")) (Just (ExpName (Name [Ident "*obj"]))))
-- wlp' lets you specify the inherited attributes
wlp' :: Inh -> Stmt -> Syn