polyver/examples/example/example.py at main · uclid-org/polyver · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
from pathlib import Path

from uclid.builder import *
from uclid.builder_sugar import *

from polyver.main import getModelChecker
from polyver.module import Module
from polyver.procedure import Procedure
from polyver.utils import Lang


class ExampleModule(Module):
    def __init__(self, delete=True, verbose=False):
        super().__init__("example", delete, verbose)
        foo = Procedure(
            name="foo",
            lang=Lang.C,
            filepath=Path(__file__).parent / "foo.c",
            jsonpath=Path(__file__).parent / "foo.json",
        )
        self.procs = {foo.name: foo}

    def buildUclidModule(self) -> UclidModule:
        bits = 32
        valType = UclidBVType(bits)
        m = UclidModule("main")
        x = m.mkVar("x", valType)
        y = m.mkVar("y", valType)
        init_y = m.mkVar("init_y", valType)
        i = UclidLiteral("i")
        r = UclidLiteral("r")
        foo_fired = m.mkVar("foo_fired", UclidBooleanType())

        requires = UclidRaw(self.procs["foo"].getLatestUclidRequiresString())
        ensures = UclidRaw(self.procs["foo"].getLatestUclidEnsuresString())
        proc_sig = UclidProcedureSig(
            inputs=[(i, valType)],
            modifies=None,
            returns=[(r, valType)],
            requires=requires,
            ensures=ensures,
            noinline=True,
        )
        foo = m.mkProcedure(
            "foo",
            proc_sig,
            UclidBlockStmt(
                [
                    UclidComment(self.procs["foo"].code),
                ]
            ),
        )

        step_sig = UclidProcedureSig(
            inputs=[],
            modifies=[x, y, init_y, foo_fired],
            returns=[],
            requires=None,
            ensures=None,
            noinline=False,
        )
        step = m.mkProcedure(
            "step",
            step_sig,
            UclidBlockStmt(
                [
                    UclidAssignStmt(x, y),
                    UclidAssignStmt(init_y, y),
                    UclidAssignStmt(foo_fired, UclidBooleanLiteral(True)),
                    self.addProcedureCallStmt(foo, [init_y], [y]),
                ]
            ),
        )

        m.setInit(
            UclidInitBlock(
                [
                    UclidAssignStmt(x, UclidBVLiteral(0, bits)),
                    UclidAssignStmt(y, UclidBVLiteral(50, bits)),
                    UclidAssignStmt(init_y, y),
                    UclidAssignStmt(foo_fired, UclidBooleanLiteral(False)),
                ]
            )
        )

        m.setNext(
            UclidNextBlock(
                [UclidProcedureCallStmt(step, [], [])]
                # [
                #     UclidAssignStmt(x.p(), y),
                #     self.addProcedureCallStmt(foo, [y], [y.p()]),
                # ]
            )
        )

        m.mkProperty("diff", Ugte([Usub([y, x]), UclidBVLiteral(50, bits)]))

        m.setControl(
            UclidControlBlock(
                [
                    UclidBMCCommand("v", 3),
                    UclidCheckCommand(),
                    UclidPrintResultsCommand(),
                    UclidPrintCexJSONCommand("v", [x, y, init_y, foo_fired]),
                ]
            )
        )

        return m


if __name__ == "__main__":
    m = ExampleModule()
    # print(m.buildUclidModule().__inject__())
    mc = getModelChecker(m)
    mc.check()
    mc.report("./result.json")