Support for deductive verification using SMTLIB Z3 solver in Chiron Framework

.gitignore

@@ -162,4 +162,7 @@ cython_debug/
 
 # Extra files and hidden folder.
 testcases/
-build/
+build/
+
+virtual/
+.vscode/

ChironCore/ChironAST/ChironAST.py

@@ -36,6 +36,13 @@ def __init__(self, condition):
     def __str__(self):
         return self.cond.__str__()
 
+class AnalysisCommand(Instruction):
+    def __init__(self, statement, condition):
+        self.stmt = statement
+        self.cond = condition
+    def __str__(self):
+        return self.stmt + " (" + self.cond.__str__() + ")"
+
 class MoveCommand(Instruction):
     def __init__(self, motion, expr):
         self.direction = motion
@@ -126,6 +133,10 @@ class Div(BinArithOp):
     def __init__(self, lexpr, rexpr):
         super().__init__(lexpr, rexpr, "/")
 
+class Mod(BinArithOp):
+    def __init__(self, lexpr, rexpr):
+        super().__init__(lexpr, rexpr, "%")
+
 
 # --Boolean Expressions-----------------------------------------------
 

ChironCore/ChironAST/builder.py

@@ -88,6 +88,8 @@ def visitMulExpr(self, ctx:tlangParser.MulExprContext):
             return ChironAST.Mult(left, right)
         elif ctx.multiplicative().DIV():
             return ChironAST.Div(left, right)
+        elif ctx.multiplicative().MOD():
+            return ChironAST.Mod(left, right)
 
 
     # Visit a parse tree produced by tlangParser#parenExpr.
@@ -97,7 +99,7 @@ def visitParenExpr(self, ctx:tlangParser.ParenExprContext):
 
     def visitCondition(self, ctx:tlangParser.ConditionContext):
         if ctx.PENCOND():
-            return ChironAST.PenStatus();
+            return ChironAST.PenStatus()
 
         if ctx.NOT():
             expr1 = self.visit(ctx.condition(0))
@@ -172,3 +174,34 @@ def visitMoveCommand(self, ctx:tlangParser.MoveCommandContext):
 
     def visitPenCommand(self, ctx:tlangParser.PenCommandContext):
         return [(ChironAST.PenCommand(ctx.getText()), 1)]
+
+    def visitAnalysisCommand(self, ctx:tlangParser.AnalysisCommandContext):
+        analysisCommand = ctx.analysisStatement().getText()
+        analysisCondition = self.visit(ctx.condition())
+        return [(ChironAST.AnalysisCommand(analysisCommand, analysisCondition), 1)]
+
+class astGenPassSMTLIB(astGenPass):
+    def __init__(self):
+        super().__init__()
+        self.repeatInstrCount = 0 # keeps count for no of 'repeat' instructions
+
+    def visitIfConditional(self, ctx:tlangParser.IfConditionalContext):
+        condObj = ChironAST.ConditionCommand(self.visit(ctx.condition()))
+        thenInstrList = self.visit(ctx.strict_ilist())
+        boolFalse = ChironAST.ConditionCommand(ChironAST.BoolFalse())
+        elseInstrList = [(boolFalse, 1)]
+        jumpOverElseBlock = [(ChironAST.ConditionCommand(ChironAST.BoolFalse()), len(elseInstrList) + 1)]
+        return [(condObj, len(thenInstrList) + 2)] + thenInstrList + jumpOverElseBlock + elseInstrList
+
+    def visitMoveCommand(self, ctx):
+        mvcommand = ctx.moveOp().getText()
+        mvexpr = self.visit(ctx.expression())
+        if mvcommand == "forward" or mvcommand == "backward":
+            return [(ChironAST.MoveCommand(mvcommand, mvexpr), 1), (ChironAST.NoOpCommand(), 1)]
+        else:
+            return super().visitMoveCommand(ctx)
+
+    def visitGotoCommand(self, ctx):
+        return [(super().visitGotoCommand(ctx)), (ChironAST.NoOpCommand(), 1)]
+
+

ChironCore/ProofEngine/Infix_To_Prefix.py

@@ -0,0 +1,159 @@
+import ast
+import re 
+
+"""
+This module provides functionality to convert infix expressions into prefix (SMT-LIB) format.
+It uses Python's `ast` module to parse expressions and a custom visitor class to traverse
+the abstract syntax tree (AST) and generate the corresponding prefix notation.
+"""
+
+class PrefixNotationConverter(ast.NodeVisitor):
+    """
+    A custom AST visitor class to convert infix expressions into prefix notation.
+    """
+
+    def visit_BinOp(self, node):
+        """
+        Handles binary operations (e.g., +, -, *, /).
+        Converts them into prefix notation (e.g., (+ left right)).
+        """
+        op = self.get_operator(node.op)
+        left = self.visit(node.left)
+        right = self.visit(node.right)
+        return f"({op} {left} {right})"
+
+    def visit_Compare(self, node):
+        """
+        Handles comparison operations (e.g., ==, !=, >, <, >=, <=).
+        Converts them into prefix notation.
+        Special handling for "!=" to represent it as (not (= left right)).
+        """
+        op = self.get_operator(node.ops[0])
+        left = self.visit(node.left)
+        right = self.visit(node.comparators[0])
+        if op == '!=':  # Handle "!=" as (not (= expr1 expr2))
+            return f"(not (= {left} {right}))"
+        else:
+            return f"({op} {left} {right})"
+
+    def visit_BoolOp(self, node):
+        """
+        Handles boolean operations (e.g., and, or).
+        Converts them into prefix notation (e.g., (and expr1 expr2 ...)).
+        """
+        op = self.get_operator(node.op)
+        values = " ".join(self.visit(value) for value in node.values)
+        return f"({op} {values})"
+
+    def visit_UnaryOp(self, node):
+        """
+        Handles unary operations (e.g., not, -).
+        Converts them into prefix notation (e.g., (not operand)).
+        """
+        op = self.get_operator(node.op)
+        operand = self.visit(node.operand)
+        return f"({op} {operand})"
+
+    def visit_Name(self, node):
+        """
+        Handles variable names.
+        Returns the variable name as is.
+        """
+        return node.id
+
+    def visit_Constant(self, node):
+        """
+        Handles constant values (e.g., numbers, strings).
+        Returns the constant value as a string.
+        """
+        return str(node.value)
+
+    def get_operator(self, op):
+        """
+        Maps Python AST operators to their corresponding SMT-LIB operators.
+        """
+        operators = {
+            ast.Add: '+',
+            ast.Sub: '-',
+            ast.Mult: '*',
+            ast.Div: 'div',
+            ast.Gt: '>',
+            ast.Lt: '<',
+            ast.GtE: '>=',
+            ast.LtE: '<=',
+            ast.Eq: '=',
+            ast.NotEq: '!=',
+            ast.Mod: 'mod',
+            ast.And: 'and',
+            ast.Or: 'or',
+            ast.Not: '~',
+            ast.Assign: '=',
+            ast.USub: '-',  # Unary subtraction
+        }
+        return operators[type(op)]
+
+def preprocess_expression(expr: str, replace_eq):
+    """
+    Preprocesses the input expression to make it compatible with Python's `ast` module.
+    - Replaces variable prefixes (e.g., ":var" -> "var").
+    - Removes spaces.
+    - Optionally replaces single "=" with "==" for equality checks.
+
+    Args:
+        expr (str): The input infix expression.
+        replace_eq (bool): Whether to replace "=" with "==" for equality.
+
+    Returns:
+        str: The preprocessed expression.
+    """
+    expr = re.sub(r":(\w+)", r"\1", expr)  # Remove ":" prefix from variables
+    expr = expr.replace(" ", "")  # Remove spaces
+    if replace_eq:
+        expr = re.sub(r"(?<![<>=!])=(?!=)", "==", expr)  # Replace "=" with "==" for equality
+    return expr
+
+def Construct_AST(expr: str, replace_eq):
+    """
+    Constructs an abstract syntax tree (AST) from the given infix expression.
+
+    Args:
+        expr (str): The input infix expression.
+        replace_eq (bool): Whether to preprocess the expression to replace "=" with "==".
+
+    Returns:
+        ast.AST: The constructed AST.
+
+    Raises:
+        Exception: If there is a syntax error in the input expression.
+    """
+    expr = preprocess_expression(expr, replace_eq)
+    # print(expr)  # Debugging print for the preprocessed expression
+    try:
+        tree = ast.parse(expr, mode='eval')  # Parse the expression in evaluation mode
+        return tree
+    except SyntaxError as e:
+        print(expr)  # Debugging print for the expression causing the error
+        raise Exception(f"Syntax Error: {e}")
+
+def Infix_To_Prefix(expr: str, replace_eq=False):
+    """
+    Converts an infix expression into prefix notation.
+
+    Args:
+        expr (str): The input infix expression.
+        replace_eq (bool): Whether to preprocess the expression to replace "=" with "==".
+
+    Returns:
+        str: The prefix notation of the expression, or None if the input is empty.
+    """
+    if expr:
+        tree = Construct_AST(expr, replace_eq)
+        if tree:
+            converter = PrefixNotationConverter()
+            expr = converter.visit(tree.body)  # Visit the root of the AST
+            return expr
+        else:
+            return None
+    else:
+        return None
+