形式化方法—作业5—EUF理论

一.背景

  课程主页: Formal Methods Foundation
  作业地址: Formal Methods Assignment5
  如果您的英文足够好,请直接点击上述链接查看相关信息
  由于课程结束上述链接失效, 请点击此处Wolai课程链接查看相关资料。

二.作业

 2.1 基本EUF逻辑

  在本节中,我们将使用 Z3 解决 EUF 理论中的基本 SMT 问题。要声明未解释的函数或变量,可以定义一个新的Sort,并从中声明变量和函数


S = DeclareSort('S')
e = Const('e', S)
f = Function('f', S, S)
g = Function('g', S, S, S)

  上面的代码声明了一个新的抽象Sort S,在S上声明了一个变量e,以及一个 S->S的函数f,即函数f接受类型S的参数,并返回类型S的值。函数g很像函数f,唯一的不同点在于函数g接受两个S类型的参数。
  鉴于上述声明,我们可以让 Z3 求解 EUF 约束,如:


solve(e != e)
solve(e == f(e))
solve(e == f(g(e, e))

  Exercise 1: 分析erexcise1文件,添加自己的限制条件并解释输出的原因,具体分析请查看注释部分

from z3 import *

# Before we presenting the EUF theory, we first introduce some Z3's
# facilities to define terms and functions.

########################################
# Sort, term, formula

# In Z3, we can define sorts, we can simply think them as sets.
# This code declares a new sort (although abstract) called S.:
S = DeclareSort('S')

# The sort can contain constants:
e = Const('e', S)

# Z3 has some builtin sort:
# Bool, Int, Real, BitVec n, Array, Index, Elem, String, Seq S.
# which can be used directly.

# We can define functions:
f = Function('f', S, S)
g = Function('g', S, S, S)
# this is a unary function from sort S to sort S.
# we can solve the congruence rule:
# e is a constant from S.

# And e has some intrinsic property, for example, the reflexivity.
# Hence, the following proposition is unsat:
solve(e != e)
#显然无解 e一定等于e

# the following propositions have solution:
solve(e == f(e))
#输出为 [e = S!val!0, f = [else -> S!val!0]]
# else -> S!val!0  f(e)==S!val!0 那么 e 一定等于f(e)

solve(e == f(g(e, e)))
#输出为[e = S!val!1, g = [else -> S!val!0], f = [else -> S!val!1]]
#g函数一定得出S!val!0 f函数一定得出S!val!1 一定等于e


# the example from the lecture:
x1, x2, x3, x4, x5 = Consts('x1 x2 x3 x4 x5', S)
solve(x1 == x2, x2 == x3, x4 == x5, x5 != x1, f(x1) != f(x3))
# with the result "no solution".
# 输出为no solution
# 圈1 x1 x2 x3
# 圈2 x4 x5
# x1 x3相等 f(x1)==f(x3) 故无解

# If we change the inequality to equality:
solve(x1 == x2, x2 == x3, x4 == x5, x5 != x1, f(x1) == f(x3))
# this will give the following solution:
'''
[x3 = S!val!1,
 x5 = S!val!0,
 x4 = S!val!0,
 x1 = S!val!1,
 x2 = S!val!1]
'''
# note that S!val!0, S!val!1 are distinct values.
# 输出为上面绿色部分内容
#  圈1 x1 x2 x3
#  圈2 x4 x5
#  同圈内元素值相等 由于x1==x3 则f(x1)==f(x3) 一定有解 只要x1 x2 x3值相等,x4 x5值相等,且这两部分值不等即可

# Let's study the translation validation we presented in the lecture:
x1, x2, y1, y2, t1, t2, z = Consts('x1 x2 y1 y2 t1 t2 z', S)
f = Function('f', S, S, S)
g = Function('g', S, S, S)
F1 = And(t1 == f(x1, y1), t2 == f(x2, y2), z == g(t1, t2))
F2 = And(z == g(f(x1, y1), f(x2, y2)))
F = Implies(F1, F2)
solve(Not(F))
# no solution
# F1 = f(x1,y1) and f(x2,y2) and g(t1,t2) F1=t1 and t2 and g(t1,t2)
# F2 = g(f(x1,y1),f(x2,y2))               F2=g(t1,t2)
# F = f(x1,y1) and f(x2,y2) and g(t1,t2) -> g(f(x1,y1)) and f(x2,y2)
solve(F)
#解为 [x2 = S!val!4,
 # t1 = S!val!9,
 # z = S!val!0,
 # y1 = S!val!2,
 # t2 = S!val!8,
 # y2 = S!val!5,
 # x1 = S!val!1,
 # f = [(S!val!4, S!val!5) -> S!val!6, else -> S!val!3],
 # g = [(S!val!9, S!val!8) -> S!val!10, else -> S!val!7]]

 #f(x2,y2)->S!val!6   f(else)->S!val!3
 #g(t1,t2)->S!val!10  g(else)->S!val!7
# F1 : S!val!9 and S!val!8 and S!val!10
# F2 : S!val!10
# 显然解正确

# Let's try another example
# This code:
f = Function('f', S, S)
x1, x2, x3, x4, x5 = Consts('x1 x2 x3 x4 x5', S)
solve(x1 == x2, x2 == x3, x4 == x5, x5 != x1, f(x1) != f(x3))
# what's Z3's output? And why that output?
# 输出 : no solution
#  圈1 x1 x2 x3
#  圈2 x4 x5
#  同一圈内值变量值相等 x1==x3 则 f(x1)==f(x3) 故无解

#自己的测试用例
print()
print("my test")
f = Function('f', S, S)
x1, x2, x3, x4, x5 = Consts('x1 x2 x3 x4 x5', S)
solve(x1 == x2, x2 == x3, x4 == x5, x5 == x1, f(x1) == f(x5))
# 输出为[x3 = S!val!0,
#  x4 = S!val!0,
#  x5 = S!val!0,
#  x1 = S!val!0,
#  x2 = S!val!0]
#  所有值相等,故有界,且每个变量为同一值


  Exercise 2: 证明函数等价
  想要证明函数等价,有一个很重要的规则


     s1=t1      ...      sn=tn
------------------------------------------- (Congruence)
     f(s1, ..., sn) = f(t1, ..., tn)

  请利用上述规则证明函数pow3与pow3_new等价

'''
int power3(int in){
  int i, out_a;
  out_a = in;
  for(i = 0; i < 2; i++)
    out_a = out_a * in;
  return out_a;
}
'''
# and the other one is:
'''
int power3_new(int in){
  int out_b;
  out_b = (in*in)*in;
  return out_b;
}
'''
###################################证明由此开始

import z3
from z3 import *

class Todo(Exception):
    def __init__(self, msg):
        self.msg = msg

    def __str__(self):
        return self.msg

    def __repr__(self):
        return self.__str__()

#声明未定义变量集合S
S=DeclareSort('S') 

#声明位定义变量
inn,out_a_0,out_a_1,out_a_2,out_b=Consts('inn out_a_0 out_a_1 out_a_2 out_b',S)

#声明函数
f=Function('f',S,S,S)

#pow3
P1=And(out_a_0==inn,out_a_1==f(out_a_0,inn),out_a_2==f(out_a_1,inn))

#pow3_new
P2=And(out_b==f(f(inn,inn),inn))
# 这是解的一种情况
print('这是解的一种情况')
solve(Implies(And(P1,P2),out_a_2==out_b))

# valid(P) <==> unsat(~P)
print('Not无解则证明恒等价')
solve(Not(Implies(And(P1,P2),out_a_2==out_b)))

 2.2 Translation validation

  在这一节中,我们将实现课堂上讨论的小型编译器的语法翻译,我们需要将源语言中的程序翻译成目标语言的等效程序,我们只需要确保确认输入输出等效即可,而无需考虑其他因素
  我们需要翻译的源语言是Calc,它是是Calculator语言的简写。该语言的上下文语法如下


bop ::= + | - | * | /
E   ::= x | E bop E
S   ::= x=E
F   ::= f(x1, …, xn){S;* return E;}

the non-terminal bop stands for an binary operator, we have a bunch of syntactic forms: 
    the addition, subtraction, multiplication, and division.

the non-terminal E stands for an expression, we have a bunch of syntactic forms: 
    a basic variable x, binary operation of two expressions.

The non-terminal S stands for a statement, there is only one syntactic form: 
    the assigment.

A function F has a sequence of arguments: x1, ..., xn, 
and its function body consists of a sequence of statement S, 
followed by a return statement, and the return statement always returns a variable x.

  Exercise 3.4.5: 阅读并分析calc.py文件,理解相关数据结构和函数的定义,请参考注释部分

from enum import Enum
from typing import List
from z3 import *
from counter import counter

class Todo(Exception):
    def __init__(self, msg):
        self.msg = msg

    def __str__(self):
        return self.msg

    def __repr__(self):
        return self.__str__()


##################################
# The abstract syntax for the Calc language:
'''
bop ::= + | - | * | /
E   ::= x | E bop E
S   ::= x=E
F   ::= f(x1, …, xn){S;* return E;}
'''


# binary operator
class BOp(Enum):
    ADD = "+"
    SUB = "-"
    MUL = "*"
    DIV = "/"


# expression
class Expr:
    def __repr__(self):
        return self.__str__()


class ExprVar(Expr):
    def __init__(self, var: str):
        self.var = var

    def __str__(self):
        return f"{self.var}"

#根据类型分别转换
class ExprBop(Expr):
    def __init__(self, left: Expr, right: Expr, bop: BOp):
        self.left = left
        self.right = right
        self.bop = bop

    def __str__(self):
        if isinstance(self.left, ExprBop):
            left_str = f"({self.left})"
        else:
            left_str = f"{self.left}"

        if isinstance(self.right, ExprBop):
            right_str = f"({self.right})"
        else:
            right_str = f"{self.right}"

        return f"{left_str} {self.bop.value} {right_str}"


# statement
class Stmt:
    def __init__(self):
        self.level = 0

    def __repr__(self):
        return self.__str__()


class StmtAssign(Stmt):
    def __init__(self, var: str, expr: Expr):
        super().__init__()
        self.var = var
        self.expr = expr

    def __str__(self):
        indent_space = self.level * "\t"
        return f"{indent_space}{self.var} = {self.expr};\n"


# function:
class Function:
    def __init__(self, name: str, args: List[str], stmts: List[Stmt], ret: str):
        self.name = name
        self.args = args
        self.stmts = stmts
        self.ret = ret

    def __str__(self):
        arg_str = ",".join(self.args)
        for stm in self.stmts:
            stm.level += 1

        stmts_str = "".join([str(stmt) for stmt in self.stmts])

        return (f"{self.name}({arg_str}){{\n"
                f"{stmts_str}"
                f"\treturn {self.ret};\n"
                f"}}\n")


###############################################
# SSA conversion:

# take a function 'func', convert it to SSA
def to_ssa_func(func: Function) -> Function:
    # a map from variable to new variable:
    # init it by putting every argument into the map
    var_map = {arg: arg for arg in func.args}

    # fresh variable generator
    fresh_var = counter(prefix=f"calc_{func.name}")

    def to_ssa_expr(expr):
        if isinstance(expr, ExprVar):
            return ExprVar(var_map[expr.var])

        if isinstance(expr, ExprBop):
            return ExprBop(to_ssa_expr(expr.left), to_ssa_expr(expr.right), expr.bop)

    def to_ssa_stmt(stmt):
        if isinstance(stmt, StmtAssign):
            new_expr = to_ssa_expr(stmt.expr)
            new_var = next(fresh_var)
            var_map[stmt.var] = new_var
            return StmtAssign(new_var, new_expr)

    # to convert each statement one by one:
    new_stmts = [to_ssa_stmt(stmt) for stmt in func.stmts]

    return Function(func.name, func.args, new_stmts, var_map[func.ret])


###############################################
# 从此开始转换为z3表达式
# Generate Z3 constraints:
def gen_cons_exp(expr: Expr):
    if isinstance(expr, ExprVar):
        return Const(expr.var, DeclareSort('S'))

    if isinstance(expr, ExprBop):
        if expr.bop is BOp.ADD:
            func_name = "f_add"
        elif expr.bop is BOp.SUB:
            func_name = "f_sub"
        elif expr.bop is BOp.MUL:
            func_name = "f_mul"
        elif expr.bop is BOp.DIV:
            func_name = "f_div"
        else:
            raise ValueError("unknown binary operator")

        left = gen_cons_exp(expr.left)
        right = gen_cons_exp(expr.right)

        return z3.Function(func_name,
                           DeclareSort('S'),
                           DeclareSort('S'),
                           DeclareSort('S')).__call__(left, right)


def gen_cons_stm(stmt):
    if isinstance(stmt, StmtAssign):
        return Const(stmt.var, DeclareSort('S')) == gen_cons_exp(stmt.expr)


def gen_cons_func(func):
    return [gen_cons_stm(stmt) for stmt in func.stmts]

# 测试功能是否正常
# a sample program:
sample_f = Function('f',
                    ['s1', 's2', 't1', 't2'],
                    [StmtAssign('z', ExprBop(ExprBop(ExprVar('s1'), ExprVar('t1'), BOp.ADD),
                                             ExprBop(ExprVar('s2'), ExprVar('t2'), BOp.ADD),
                                             BOp.MUL)),
                     StmtAssign('z', ExprBop(ExprVar('z'), ExprVar('s1'), BOp.MUL))],
                    'z')

if __name__ == '__main__':
    # print the original program
    print(sample_f)
    # convert it to SSA
    new_f = to_ssa_func(sample_f)
    # print the converted program
    print(new_f)
    # generate Z3 constraints
    print(gen_cons_func(new_f))

  Exercise 6.7.8: 仿照calc.py实现如下语法tac


S ::= x=y | x=y+z | x=y-z | x=y*z | x=y/z
F ::= f(x1, ..., xn){S;* return x;}

import unittest
from z3 import *
from counter import counter

class Todo(Exception):
    def __init__(self, msg):
        self.msg = msg

    def __str__(self):
        return self.msg

    def __repr__(self):
        return self.__str__()

##################################
# The abstract syntax for the Tac (three address code) language:
"""
S ::= x=y | x=y+z | x=y-z | x=y*z | x=y/z
F ::= f(x1, ..., xn){S;* return x;}
"""

# statement
class Stmt:
    def __repr__(self):
        return self.__str__()

#定义部分没啥说的 根据语法参考calc即可
class StmtAssignVar(Stmt):
    def __init__(self, x, y):
        self.x = x
        self.y = y

    def __str__(self):
        # raise Todo("Exercise 6: finish the __str__ method in data structure StmtAssignVar")

        return f"{self.x} = {self.y};\n"


class StmtAssignAdd(Stmt):
    def __init__(self, x, y, z):
        self.x = x
        self.y = y
        self.z = z

    def __str__(self):
        # raise Todo("Exercise 6: finish the __str__ method in data structure StmtAssignAdd")
        return f"{self.x} = {self.y} + {self.z};\n"


class StmtAssignSub(Stmt):
    def __init__(self, x, y, z):
        self.x = x
        self.y = y
        self.z = z

    def __str__(self):
        # raise Todo("Exercise 6: finish the __str__ method in data structure StmtAssignSub")
        return f"{self.x} = {self.y} - {self.z};\n"


class StmtAssignMul(Stmt):
    def __init__(self, x, y, z):
        self.x = x
        self.y = y
        self.z = z

    def __str__(self):
        # raise Todo("Exercise 6: finish the __str__ method in data structure StmtAssignMul")
        return f"{self.x} = {self.y} * {self.z};\n"


class StmtAssignDiv(Stmt):
    def __init__(self, x, y, z):
        self.x = x
        self.y = y
        self.z = z

    def __str__(self):
        # raise Todo("Exercise 6: finish the __str__ method in data structure StmtAssignDiv")
        return f"{self.x} = {self.y} / {self.z};\n"

# function:
class Function:
    def __init__(self, name, args, stmts, ret):
        self.name = name
        self.args = args
        self.stmts = stmts
        self.ret = ret

    def __str__(self):
        # raise Todo("Exercise 6: finish the __str__ method in data structure Function")
        arg_str = ",".join(self.args)
        stmts_str = "\t".join([str(stmt) for stmt in self.stmts])
        return (f"{self.name}({arg_str}){{\n"
                f"\t{stmts_str}"
                f"\treturn {self.ret};\n"
                f"}}\n")


###############################################
# SSA conversion:

# take a function 'f', convert it to SSA
def to_ssa_func(func: Function) -> Function:
    # raise Todo("Exercise 7: do SSA conversion on tac function ")
    # 记录已经处理过的变量
    var_map = {arg: arg for arg in func.args}
    # fresh variable generator
    fresh_var = counter(prefix=f"tac_{func.name}")

    def to_ssa_stmt(stmt):
        # raise Todo("Exercise 7: do SSA conversion on tac statements ")
        # 左边一定要一个新参数名,注意存入字典
        # 右边需要判断是否在字典中存在,不存在则分配新的,注意分配完后存入字典
        if isinstance(stmt, StmtAssignVar):
            new_var = next(fresh_var)
            var_map[stmt.x] = new_var
            if stmt.y not in var_map:
                new_var1 = next(fresh_var)
                var_map[stmt.y] = new_var1
            else: new_var1=var_map[stmt.y]
            return StmtAssignVar(new_var, new_var1)

        # 加法
        elif isinstance(stmt, StmtAssignAdd):
            new_var = next(fresh_var)
            var_map[stmt.x] = new_var
            if stmt.y not in var_map:
                new_var1 = next(fresh_var)
                var_map[stmt.y] = new_var1
            else:
                new_var1 = var_map[stmt.y]
            if stmt.z not in var_map:
                new_var2 = next(fresh_var)
                var_map[stmt.z] = new_var2
            else:
                new_var2 = var_map[stmt.z]
            return StmtAssignAdd(new_var,new_var1,new_var2)
        
        # 乘法
        elif isinstance(stmt, StmtAssignMul):
            new_var = next(fresh_var)
            var_map[stmt.x] = new_var
            if stmt.y not in var_map:
                new_var1 = next(fresh_var)
                var_map[stmt.y] = new_var1
            else:
                new_var1 = var_map[stmt.y]
            if stmt.z not in var_map:
                new_var2 = next(fresh_var)
                var_map[stmt.z] = new_var2
            else:
                new_var2 = var_map[stmt.z]
            return StmtAssignMul(new_var, new_var1, new_var2)
        
        # 除法
        elif isinstance(stmt, StmtAssignDiv):
            new_var = next(fresh_var)
            var_map[stmt.x] = new_var
            if stmt.y not in var_map:
                new_var1 = next(fresh_var)
                var_map[stmt.y] = new_var1
            else:
                new_var1 = var_map[stmt.y]
            if stmt.z not in var_map:
                new_var2 = next(fresh_var)
                var_map[stmt.z] = new_var2
            else:
                new_var2 = var_map[stmt.z]
            return StmtAssignDiv(new_var, new_var1, new_var2)
        
        # 减法
        elif isinstance(stmt, StmtAssignSub):
            new_var = next(fresh_var)
            var_map[stmt.x] = new_var
            if stmt.y not in var_map:
                new_var1 = next(fresh_var)
                var_map[stmt.y] = new_var1
            else:
                new_var1 = var_map[stmt.y]
            if stmt.z not in var_map:
                new_var2 = next(fresh_var)
                var_map[stmt.z] = new_var2
            else:
                new_var2 = var_map[stmt.z]
            return StmtAssignSub(new_var, new_var1, new_var2)


            # to convert each statement one by one:
    new_stmts = [to_ssa_stmt(stmt) for stmt in func.stmts]
    return Function(func.name, func.args, new_stmts, var_map[func.ret])

###############################################
# Generate Z3 constraints:
def gen_cons_stmt(stmt):
    # raise Todo("Exercise 8: generate constraints form TAC statements ")
    # 约束条件,注意变量个数,别的就没啥了,参考calc就可以了,转化为z3表达式
    if isinstance(stmt, StmtAssignVar):
        return Const(stmt.x, DeclareSort('S')) == Const(stmt.y, DeclareSort('S'))
    if isinstance(stmt, StmtAssignAdd):
        return Const(stmt.x, DeclareSort('S')) ==z3.Function('f_add',
                           DeclareSort('S'),
                           DeclareSort('S'),
                           DeclareSort('S')).__call__(Const(stmt.y,DeclareSort('S')),Const(stmt.z,DeclareSort('S')))
    if isinstance(stmt, StmtAssignDiv):
        return Const(stmt.x, DeclareSort('S')) ==z3.Function('f_div',
                           DeclareSort('S'),
                           DeclareSort('S'),
                           DeclareSort('S')).__call__(Const(stmt.y,DeclareSort('S')),Const(stmt.z,DeclareSort('S')))
    if isinstance(stmt, StmtAssignMul):
        return Const(stmt.x, DeclareSort('S')) ==z3.Function('f_mul',
                           DeclareSort('S'),
                           DeclareSort('S'),
                           DeclareSort('S')).__call__(Const(stmt.y,DeclareSort('S')),Const(stmt.z,DeclareSort('S')))
    if isinstance(stmt, StmtAssignSub):
        return Const(stmt.x, DeclareSort('S')) ==z3.Function('f_sub',
                           DeclareSort('S'),
                           DeclareSort('S'),
                           DeclareSort('S')).__call__(Const(stmt.y,DeclareSort('S')),Const(stmt.z,DeclareSort('S')))



def gen_cons_func(func):
    # raise Todo("Exercise 8: generate constraints form TAC function ")
    return [gen_cons_stmt(stmt) for stmt in func.stmts]

###############################################
# Tests
# 测试,注释部分为正确输出
test_case = Function('f',
                     ['s1', 's2', 't1', 't2'],
                     [StmtAssignAdd('a', 's1', 't1'),
                      StmtAssignAdd('b', 's2', 't2'),
                      StmtAssignMul('c', 'a', 'b'),
                      StmtAssignMul('b', 'c', 's1'),
                      StmtAssignVar('z', 'b')],
                     'z')


class TestTac(unittest.TestCase):
    ssa = to_ssa_func(test_case)
    cons = gen_cons_func(ssa)

    def test_print(self):
        res = ("f(s1,s2,t1,t2){\n\ta = s1 + t1;\n\tb = s2 + t2;\n\tc = a * b;\n\t"
               "b = c * s1;\n\tz = b;\n\treturn z;\n}\n")

        # f(s1, s2, t1, t2){
        #   a = s1 + t1;
        #   b = s2 + t2;
        #   c = a * b;
        #   b = c * s1;
        #   z = b;
        #   return z;
        # }
        print(test_case)
        self.assertEqual(str(test_case), res)

    def test_to_ssa(self):
        res = ("f(s1,s2,t1,t2){\n\t_tac_f_0 = s1 + t1;\n\t_tac_f_1 = s2 + t2;\n\t_tac_f_2 = _tac_f_0 * _tac_f_1;\n\t"
               "_tac_f_3 = _tac_f_2 * s1;\n\t_tac_f_4 = _tac_f_3;\n\treturn _tac_f_4;\n}\n")

        # f(s1, s2, t1, t2){
        #   _tac_f_0 = s1 + t1;
        #   _tac_f_1 = s2 + t2;
        #   _tac_f_2 = _tac_f_0 * _tac_f_1;
        #   _tac_f_3 = _tac_f_2 * s1;
        #   _tac_f_4 = _tac_f_3;
        #   return _tac_f_4;
        # }

        print(self.ssa)
        self.assertEqual(str(self.ssa), res)

    def test_gen_cons(self):
        res = ("[_tac_f_0 == f_add(s1, t1),"
               " _tac_f_1 == f_add(s2, t2),"
               " _tac_f_2 == f_mul(_tac_f_0, _tac_f_1),"
               " _tac_f_3 == f_mul(_tac_f_2, s1),"
               " _tac_f_4 == _tac_f_3]")
        print(self.cons)
        self.assertEqual(str(self.cons), res)

if __name__ == '__main__':
    unittest.main()

  Exercise 9.10: 有了源语言calc和目标语言tac,我们需要实现源语言到目标语言的编译器,在本实验中,你只需要实现以下三个函数即可
      compile_func():编译一个函数;
      compile_stmt():编译语句;
      compile_expr():编译一个表达式;
  实现功能后,请填写函数translation_validation()中缺少的代码,用compiler.py 完成翻译验证程序并测试您的实现。
  详细解释请参考注释部分

import unittest
from z3 import *
import calc
import tac
from counter import counter


class Todo(Exception):
    def __init__(self, msg):
        self.msg = msg

    def __str__(self):
        return self.msg

    def __repr__(self):
        return self.__str__()


###############################################
# a compiler from Calc to Tac.


def compile_func(func: calc.Function) -> tac.Function:
    tac_stmts = []
    fresh_var = counter(f"tmp_{func.name}")
    # var_map = {arg: arg for arg in func.args}

    def compile_expr(expr):
        if isinstance(expr, calc.ExprVar):
            return expr.var
        elif isinstance(expr, calc.ExprBop):
            # 注意顺序,如果直接分配由于最外层符号为*,答案tmp_0,temp_1,tmp_2顺序会有问题,测试不相等
            # 因此先把左右转换成生成变量
            newleft = compile_expr(expr.left)
            newright = compile_expr(expr.right)
            # 根据符号,判断转换后的类型,添加进条件数组
            if(expr.bop is calc.BOp.ADD):
                newvar = next(fresh_var)
                tac_stmts.append(tac.StmtAssignAdd(newvar, newleft, newright))
                return newvar
            elif (expr.bop is calc.BOp.DIV):
                newvar = next(fresh_var)
                tac_stmts.append(tac.StmtAssignDiv(newvar, newleft, newright))
                return newvar
            elif (expr.bop is calc.BOp.MUL):
                newvar = next(fresh_var)
                tac_stmts.append(tac.StmtAssignMul(newvar, newleft, newright))
                return newvar
            elif (expr.bop is calc.BOp.SUB):
                newvar = next(fresh_var)
                tac_stmts.append(tac.StmtAssignSub(newvar, newleft, newright))
                return newvar


        # raise Todo("Exercise 9: compile Calc expressions to Tac statements")

    def compile_stmt(stmt):
        if isinstance(stmt, calc.StmtAssign):
            tac_stmts.append(tac.StmtAssignVar(stmt.var, compile_expr(stmt.expr)))



    for calc_stmt in func.stmts:
        compile_stmt(calc_stmt)
    return tac.Function(func.name, func.args, tac_stmts, func.ret)


def translation_validation(original_func: calc.Function, result_func: tac.Function):
    # TODO: for the compiler to be correct, you should prove this condition:
    # TODO:     orig_cons /\ result_cons -> x1==x2
    # TODO: your code here:

    # 使用calc与tac中的函数转换功能,生成条件
    original_func_ssa = calc.to_ssa_func(original_func)
    result_func_ssa = tac.to_ssa_func(result_func)

    original_cons = calc.gen_cons_func(original_func_ssa)
    result_cons = tac.gen_cons_func(result_func_ssa)

    # 条件数组拼接
    # original_cons=original_cons+result_cons
    F1=And(original_cons+result_cons)
    solver = Solver()

    # raise Todo("Exercise 9: do the translation validation by proving this condition: orig_cons /\ result_cons -> x1==x2")
    # note that the z3.And() can accept list of constraints
    # 把表达式添加进判断器中,z3可以通过list批量添加


    #初始返回值
    res1=original_func_ssa.ret
    #结果返回值
    res2=result_func_ssa.ret
    #生成表达式
    var = tac.StmtAssignVar(res1,res2)
    #表达式转化为z3条件
    acc=tac.gen_cons_stmt(var)

    # solver.add(Not(Implies(F1,original_func.ret==result_func.ret)))
    solver.add(Not(Implies(F1, acc)))

    return solver


###############################################
# Tests
# 注释部分为正确输出,最终测试控制台应显示ok

class TestTV(unittest.TestCase):

    tac_func = compile_func(calc.sample_f)

    def test_compile(self):
        res = ("f(s1,s2,t1,t2){\n\t_tmp_f_0 = s1 + t1;\n\t_tmp_f_1 = s2 + t2;\n\t"
               "_tmp_f_2 = _tmp_f_0 * _tmp_f_1;\n\tz = _tmp_f_2;\n\t_tmp_f_3 = z * s1;\n\t"
               "z = _tmp_f_3;\n\treturn z;\n}\n")

        # f(s1, s2, t1, t2){
        #   _tac_f_0 = s1 + t1;
        #   _tac_f_1 = s2 + t2;
        #   _tac_f_2 = _tac_f_0 * _tac_f_1;
        #   _tac_f_3 = _tac_f_2;
        #   _tac_f_4 = _tac_f_3 * s1;
        #   _tac_f_5 = _tac_f_4;
        #   return _tac_f_5;
        # }
        print(tac.to_ssa_func(self.tac_func))
        self.assertEqual(str(self.tac_func), res)

    def test_tv(self):
        solver = translation_validation(calc.sample_f, self.tac_func)

        # [Not(Implies(And(_calc_f_0 ==
        #                  f_mul(f_add(s1, t1), f_add(s2, t2)),
        #                  _calc_f_1 == f_mul(_calc_f_0, s1),
        #                  _tac_f_0 == f_add(s1, t1),
        #                  _tac_f_1 == f_add(s2, t2),
        #                  _tac_f_2 == f_mul(_tac_f_0, _tac_f_1),
        #                  _tac_f_3 == _tac_f_2,
        #                  _tac_f_4 == f_mul(_tac_f_3, s1),
        #                  _tac_f_5 == _tac_f_4),
        #              _calc_f_1 == _tac_f_5))]
        print(solver)

        self.assertEqual(str(solver.check()), "unsat")


if __name__ == '__main__':
    unittest.main()

三.下载链接

  在线下载: 请点击这儿下载
  如果下载失败,点击此百度云链接:形式化方法作业五,提取码y825
  如果您有任何疑问,请通过邮箱联系我

end
  • 作者:Yuan(联系作者)
  • 发表时间:2021-12-31 18:10
  • 版权声明:自由转载-非商用-非衍生-保持署名(创意共享3.0许可证)
  • 转载声明:如果是转载博主转载的文章,请附上原文链接
  • 公众号转载:请联系作者
  • 评论

    夜风
    功能测试