/
iic.go
129 lines (118 loc) · 3.5 KB
/
iic.go
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
118
119
120
121
122
123
124
125
126
127
128
129
// Copyright 2018 Scott Cotton. All rights reserved. Use of this source
// code is governed by a license that can be found in the License file.
package main
import (
"flag"
"fmt"
"log"
"os"
"time"
"github.com/go-air/reach"
"github.com/go-air/reach/iic"
)
var iicCmd = &subCmd{
Name: "iic",
Flags: flag.NewFlagSet("iic", flag.ExitOnError),
Run: doIic,
Init: initIic,
Usage: "reach iic [options] <aiger0> [<aiger1>, ...]",
Short: "iic is an incremental inductive checker.",
Long: `
iic runs an incremental inductive checker on the supplied aiger files to find
or disprove reachability of bad states. Iic can find and output deep
counterexample traces and output inductive invariants as a witness to
unreachable bad states.
iic counterexamples are not necessarily shortest counterexamples. Bad state
depths for traces are the trace length itself. For unknown results, depths
represent the depth to which it is known no counterexample trace exists.
`}
var iicOpts = struct {
Dur *time.Duration
MaxDepth *int
Verbose *bool
Justify *bool
ConsecSift *bool
ConsecSiftPull *bool
FilterObs *bool
Preprocess *bool
}{}
func initIic(cmd *subCmd) {
flags := cmd.Flags
iicOpts.Dur = flags.Duration("dur", 30*time.Second, "timeout.")
iicOpts.MaxDepth = flags.Int("to", 1<<30, "maximum depth.")
iicOpts.Verbose = flags.Bool("v", false, "run with verbosity.")
iicOpts.Justify = flags.Bool("justify", true, "justify proof obligations.")
iicOpts.ConsecSift = flags.Bool("csift", true, "do consecutive sifting.")
iicOpts.ConsecSiftPull = flags.Bool("pull", true, "do pulling with consecutive sifting.")
iicOpts.FilterObs = flags.Bool("filter", true, "filter proof obligations.")
iicOpts.Preprocess = flags.Bool("pp", true, "pre-process aig.")
flags.StringVar(&outDir, "o", ".", "output directory")
flags.Usage = func() {
fmt.Println(cmd.Usage)
flags.PrintDefaults()
fmt.Println(cmd.Long)
}
}
func doIic(cmd *subCmd, args []string) {
flags := cmd.Flags
flags.Parse(args)
if flags.NArg() == 0 {
fmt.Fprintf(os.Stderr, "no aigs specified.\n")
}
for i := 0; i < flags.NArg(); i++ {
arg := flags.Arg(i)
if err := doIicAiger(arg, *iicOpts.Dur); err != nil {
fmt.Fprintf(os.Stderr, "error doing '%s': %s\n", arg, err)
continue
}
}
}
func doIicAiger(fn string, dur time.Duration) error {
start := time.Now()
aig, err := readAiger(fn)
if err != nil {
return err
}
fmt.Printf("read %s in %s\n", fn, time.Since(start))
bad := aigerBad(aig)
if len(bad) == 0 {
return fmt.Errorf("ErrNoBads")
}
trans := aig.S
for _, b := range bad {
mc := iic.New(trans, b)
if *iicOpts.Verbose {
fmt.Printf("created mc in %s\n", time.Since(start))
}
opts := mc.Options()
opts.Verbose = *iicOpts.Verbose
opts.Justify = *iicOpts.Justify
opts.Preprocess = *iicOpts.Preprocess
opts.Duration = *iicOpts.Dur
opts.ConsecuSift = *iicOpts.ConsecSift
opts.ConsecuSiftPull = *iicOpts.ConsecSiftPull
opts.FilterObs = *iicOpts.FilterObs
opts.MaxDepth = *iicOpts.MaxDepth
switch mc.Try() {
case 1:
fmt.Printf("%s: cex found.\n", fn)
case -1:
fmt.Printf("%s: inv found.\n", fn)
case 0:
fmt.Printf("%s: timeout.\n", fn)
default:
panic("unreachable")
}
out, err := reach.MakeOutput(fn, outDir)
if err != nil {
log.Printf("%s: error making output: %s", fn, err)
continue
}
mc.FillOutput(out)
if err := out.Store(); err != nil {
log.Printf("error storing output: %s", err)
}
fmt.Printf("wrote results in %s.\n", out.RootDir())
}
return nil
}