rustproof_libsmt/backends/
smtlib2.rs

1//! Module that contains SMTLib Backend Implementation.
2//!
3//! This backend outputs the constraints in standard smt-lib2 format. Hence,
4//! any solver that supports this format maybe used to solve for constraints.
5
6use std::process::{Child};
7use std::collections::{HashMap};
8use std::io::{Read, Write};
9
10use petgraph::graph::{Graph, NodeIndex};
11use petgraph::EdgeDirection;
12
13use backends::backend::{Logic, SMTBackend, SMTNode, SMTResult};
14use super::backend::SMTRes;
15
16/// Trait that needs to be implemented in order to support a new solver. `SMTProc` is short for
17/// "SMT Process".
18///
19/// To support a new solver that accepts input in the standard SMTLIB2 format, it is sufficient to
20/// implement this trait for the struct. This trait describes method needed to spawn, and
21/// communicate (read / write) with the solver.
22///
23/// `read` and `write` methods are implemented by deafult and needs to be changed only if the
24/// mode of communication is different (other than process pipes), or if some custom functionality
25/// is required for the specific solver.
26pub trait SMTProc {
27    /// Function to initialize the solver. This includes spawning a process and keeping the process
28    /// pipe open for read and write. The function takes &mut self as an argument to allow
29    /// configuration during initialization.
30    fn init(&mut self);
31    /// Return a mutable reference to the process pipe.
32    fn pipe<'a>(&'a mut self) -> &'a mut Child;
33
34    fn write<T: AsRef<str>>(&mut self, s: T) -> Result<(), String> {
35        // TODO: Check for errors.
36        if let Some(ref mut stdin) = self.pipe().stdin.as_mut() {
37            stdin.write(s.as_ref().as_bytes()).expect("Write to stdin failed");
38            stdin.flush().expect("Failed to flush stdin");
39        }
40        Ok(())
41    }
42
43    fn read(&mut self) -> String {
44        // XXX: This read may block indefinitely if there is nothing on the pipe to be
45        // read. To prevent this we need a timeout mechanism after which we should
46        // return with
47        // an error, such as: ErrTimeout.
48        // Another important point to note here is that, if the data available to read
49        // is exactly
50        // 2048 bytes, then this reading mechanism fails and will end up waiting to
51        // read more data
52        // (when none is available) indefinitely.
53        let mut bytes_read = [0; 2048];
54        let mut s = String::new();
55        let solver = self.pipe();
56        if let Some(ref mut stdout) = solver.stdout.as_mut() {
57            loop {
58                let n = stdout.read(&mut bytes_read).unwrap();
59                s = format!("{}{}",
60                            s,
61                            String::from_utf8(bytes_read[0..n].to_vec()).unwrap());
62                if n < 2048 {
63                    break;
64                }
65            }
66        }
67        s
68    }
69
70    // A specific read taylored to output from (check-sat) z3 command
71    fn read_checksat_output(&mut self) -> String {
72        // Buffer to read into
73        let mut buf = String::new();
74        // Read from z3's stdout
75        if let Some(ref mut stdout) = self.pipe().stdout.as_mut() {
76            loop {
77                for (_,c) in stdout.bytes().enumerate() {
78                    let chr = c.unwrap() as char;
79                    buf.push(chr);
80                    if buf.ends_with("sat") {
81                        return buf;
82                    }
83                }
84            }
85        }
86        unreachable!()
87    }
88
89    // A specific read taylored to output from (get-model) z3 command
90    fn read_getmodel_output(&mut self) -> String {
91        // Buffer to read into
92        let mut buf = String::new();
93        // Read from z3's stdout
94        if let Some(ref mut stdout) = self.pipe().stdout.as_mut() {
95            // Count for paren matching (to detect end of output)
96            let mut count = 0;
97            loop {
98                for (_,c) in stdout.bytes().enumerate() {
99                    let chr = c.unwrap() as char;
100                    // Hotfix to deal with newline remaining in the buffer
101                    if chr=='\n' && count==0 {
102                        continue;
103                    }
104                    buf.push(chr);
105                    match chr {
106                        '(' => { count+=1; },
107                        ')' => { count-=1; },
108                        _ => {}
109                    }
110                    if count==0 {
111                        return buf;
112                    }
113                }
114            }
115        }
116        unreachable!()
117    }
118
119}
120
121#[derive(Clone, Debug)]
122pub enum EdgeData {
123    EdgeOrder(usize),
124}
125
126#[derive(Clone, Debug)]
127pub struct SMTLib2<T: Logic> {
128    logic: Option<T>,
129    gr: Graph<T::Fns, EdgeData>,
130    var_index: usize,
131    var_map: HashMap<String, (NodeIndex, T::Sorts)>,
132    idx_map: HashMap<NodeIndex, String>,
133}
134
135impl<L: Logic> SMTLib2<L> {
136    pub fn new(logic: Option<L>) -> SMTLib2<L> {
137        let solver = SMTLib2 {
138            logic: logic,
139            gr: Graph::new(),
140            var_index: 0,
141            var_map: HashMap::new(),
142            idx_map: HashMap::new(),
143        };
144        solver
145    }
146
147    // Recursive function that builds up the assertion string from the tree.
148    pub fn expand_assertion(&self, ni: NodeIndex) -> String {
149        let mut children = self.gr
150                               .edges_directed(ni, EdgeDirection::Outgoing)
151                               .map(|(other, edge)| {
152                                   match *edge {
153                                       EdgeData::EdgeOrder(ref i) => (other, *i),
154                                   }
155                               })
156                               .collect::<Vec<_>>();
157        children.sort_by(|x, y| (x.1).cmp(&y.1));
158
159        let mut assertion = self.gr[ni].to_string();
160
161        assertion = if self.gr[ni].is_fn() {
162            format!("({}", assertion)
163        } else {
164            assertion
165        };
166
167        for node in &children {
168            assertion = format!("{} {}", assertion, self.expand_assertion(node.0))
169        }
170
171        if self.gr[ni].is_fn() {
172            format!("{})", assertion)
173        } else {
174            assertion
175        }
176    }
177
178    pub fn new_const<T: Into<L::Fns>>(&mut self, cval: T) -> NodeIndex {
179        self.gr.add_node(cval.into())
180    }
181}
182
183impl<L: Logic> SMTBackend for SMTLib2<L> {
184    type Idx = NodeIndex;
185    type Logic = L;
186
187    fn new_var<T, P>(&mut self, var_name: Option<T>, ty: P) -> Self::Idx
188        where T: AsRef<str>,
189              P: Into<<<Self as SMTBackend>::Logic as Logic>::Sorts>
190    {
191        let var_name = var_name.map(|s| s.as_ref().to_owned()).unwrap_or({
192            self.var_index += 1;
193            format!("X_{}", self.var_index)
194        });
195        let typ = ty.into();
196        let idx = self.gr.add_node(Self::Logic::free_var(var_name.clone(), typ.clone()));
197        self.var_map.insert(var_name.clone(), (idx, typ));
198        self.idx_map.insert(idx, var_name);
199        idx
200    }
201
202    fn set_logic<S: SMTProc>(&mut self, smt_proc: &mut S) {
203        if self.logic.is_none() {
204            return;
205        }
206        let logic = self.logic.unwrap().clone();
207        smt_proc.write(format!("(set-logic {})\n", logic));
208    }
209
210    fn assert<T: Into<L::Fns>>(&mut self, assert: T, ops: &[Self::Idx]) -> Self::Idx {
211        // TODO: Check correctness like operator arity.
212        let assertion = self.gr.add_node(assert.into());
213        for (i, op) in ops.iter().enumerate() {
214            self.gr.add_edge(assertion, *op, EdgeData::EdgeOrder(i));
215        }
216        assertion
217    }
218
219    fn check_sat<S: SMTProc>(&mut self, smt_proc: &mut S, debug: bool) -> SMTRes {
220        // Write out all variable definitions.
221        let mut decls = Vec::new();
222        for (name, val) in &self.var_map {
223            let ni = &val.0;
224            let ty = &val.1;
225            if self.gr[*ni].is_var() {
226                decls.push(format!("(declare-fun {} () {})\n", name, ty));
227            }
228        }
229        // Identify root nodes and generate the assertion strings.
230        let mut assertions = Vec::new();
231        for idx in self.gr.node_indices() {
232            if self.gr.edges_directed(idx, EdgeDirection::Incoming).collect::<Vec<_>>().is_empty() {
233                if self.gr[idx].is_fn() {
234                    assertions.push(format!("(assert {})\n", self.expand_assertion(idx)));
235                }
236            }
237        }
238
239        for w in decls.iter().chain(assertions.iter()) {
240            if debug { print!("{}", w) };
241            smt_proc.write(w);
242        }
243
244        smt_proc.write("(check-sat)\n".to_owned());
245        let read = smt_proc.read_checksat_output();
246        if &read == "sat" {
247            SMTRes::Sat(read, None)
248        } else if &read == "unsat" {
249            SMTRes::Unsat(read, None)
250        } else {
251            SMTRes::Error(read, None)
252        }
253    }
254
255    // TODO: Return type information along with the value.
256    fn solve<S: SMTProc>(&mut self, smt_proc: &mut S, debug: bool) -> (SMTResult<HashMap<Self::Idx, u64>>, SMTRes) {
257        let mut result = HashMap::new();
258        let check_sat = self.check_sat(smt_proc, debug);
259        // If the VC was satisfyable get the model
260        match check_sat {
261            SMTRes::Sat(ref res, _) => {
262                smt_proc.write("(get-model)\n".to_owned());
263                let read_result = smt_proc.read_getmodel_output();
264                return (Ok(result), SMTRes::Sat(res.clone(), Some(read_result)));
265            },
266            _ => {}
267        }
268
269        (Ok(result), check_sat.clone())
270    }
271}
rustproof_libsmt/backends/smtlib2.rs

rustproof_libsmt/backends/
smtlib2.rs
