liquid_fixpoint/
lib.rs

1//! This crate implements an interface to the [liquid-fixpoint] binary
2//!
3//! [liquid-fixpoint]: https://github.com/ucsd-progsys/liquid-fixpoint
4#![cfg_attr(feature = "nightly", feature(rustc_private))]
5
6#[cfg(feature = "nightly")]
7extern crate rustc_macros;
8#[cfg(feature = "nightly")]
9extern crate rustc_serialize;
10#[cfg(feature = "nightly")]
11extern crate rustc_span;
12
13mod constraint;
14mod constraint_fragments;
15mod constraint_solving;
16mod constraint_with_env;
17mod cstr2smt2;
18mod format;
19mod graph;
20mod parser;
21mod sexp;
22
23use std::{
24    collections::hash_map::DefaultHasher,
25    fmt::{self, Debug},
26    hash::{Hash, Hasher},
27    io::{self, BufWriter, Write as IOWrite},
28    process::{Command, Stdio},
29    str::FromStr,
30};
31
32pub use constraint::{
33    BinOp, BinRel, Bind, Constant, Constraint, DataCtor, DataDecl, DataField, Expr, Pred,
34    Qualifier, Sort, SortCtor,
35};
36pub use cstr2smt2::is_constraint_satisfiable;
37use derive_where::derive_where;
38pub use parser::parse_constraint_with_kvars;
39#[cfg(feature = "nightly")]
40use rustc_macros::{Decodable, Encodable};
41use serde::{Deserialize, Serialize, de};
42
43pub trait Types {
44    type Sort: Identifier + Hash + Clone + Debug;
45    type KVar: Identifier + Hash + Clone + Debug + Eq;
46    type Var: Identifier + Hash + Clone + Debug + PartialEq;
47    type Decimal: FixpointFmt + Hash + Clone + Debug;
48    type String: FixpointFmt + Hash + Clone + Debug;
49    type Tag: fmt::Display + FromStr + Hash + Clone + Debug;
50}
51
52pub trait FixpointFmt: Sized {
53    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result;
54
55    /// Returns a type that implements [`fmt::Display`] using this [`FixpointFmt::fmt`] implementation.
56    fn display(&self) -> impl fmt::Display {
57        struct DisplayAdapter<T>(T);
58        impl<T: FixpointFmt> std::fmt::Display for DisplayAdapter<&T> {
59            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
60                FixpointFmt::fmt(self.0, f)
61            }
62        }
63        DisplayAdapter(self)
64    }
65}
66
67pub trait Identifier: Sized {
68    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result;
69
70    /// Returns a type that implements [`fmt::Display`] using this [`Identifier::fmt`] implementation.
71    fn display(&self) -> impl fmt::Display {
72        struct DisplayAdapter<T>(T);
73        impl<T: Identifier> fmt::Display for DisplayAdapter<&T> {
74            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
75                Identifier::fmt(self.0, f)
76            }
77        }
78        DisplayAdapter(self)
79    }
80}
81
82struct DefaultTypes;
83
84impl Types for DefaultTypes {
85    type Sort = &'static str;
86    type KVar = &'static str;
87    type Var = &'static str;
88    type Tag = String;
89    type Decimal = u32;
90    type String = String;
91}
92
93impl Identifier for &str {
94    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
95        write!(f, "{self}")
96    }
97}
98
99impl FixpointFmt for u32 {
100    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
101        write!(f, "{self}")
102    }
103}
104
105impl FixpointFmt for String {
106    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
107        write!(f, "\"{self}\"")
108    }
109}
110
111#[macro_export]
112macro_rules! declare_types {
113    (   type Sort = $sort:ty;
114        type KVar = $kvar:ty;
115        type Var = $var:ty;
116        type Decimal = $real:ty;
117        type String = $str:ty;
118
119        type Tag = $tag:ty;
120    ) => {
121        pub mod fixpoint_generated {
122            pub struct FixpointTypes;
123            pub type Expr = $crate::Expr<FixpointTypes>;
124            pub type Pred = $crate::Pred<FixpointTypes>;
125            pub type Constraint = $crate::Constraint<FixpointTypes>;
126            pub type KVarDecl = $crate::KVarDecl<FixpointTypes>;
127            pub type ConstDecl = $crate::ConstDecl<FixpointTypes>;
128            pub type FunDef = $crate::FunDef<FixpointTypes>;
129            pub type Task = $crate::Task<FixpointTypes>;
130            pub type Qualifier = $crate::Qualifier<FixpointTypes>;
131            pub type Sort = $crate::Sort<FixpointTypes>;
132            pub type SortCtor = $crate::SortCtor<FixpointTypes>;
133            pub type DataDecl = $crate::DataDecl<FixpointTypes>;
134            pub type DataCtor = $crate::DataCtor<FixpointTypes>;
135            pub type DataField = $crate::DataField<FixpointTypes>;
136            pub type Bind = $crate::Bind<FixpointTypes>;
137            pub type Constant = $crate::Constant<FixpointTypes>;
138            pub use $crate::{BinOp, BinRel, ThyFunc};
139        }
140
141        impl $crate::Types for fixpoint_generated::FixpointTypes {
142            type Sort = $sort;
143            type KVar = $kvar;
144            type Var = $var;
145
146            type Decimal = $real;
147            type String = $str;
148
149            type Tag = $tag;
150        }
151    };
152}
153
154#[derive_where(Hash)]
155pub struct ConstDecl<T: Types> {
156    pub name: T::Var,
157    pub sort: Sort<T>,
158    #[derive_where(skip)]
159    pub comment: Option<String>,
160}
161
162#[derive_where(Hash)]
163pub struct FunDef<T: Types> {
164    pub name: T::Var,
165    pub args: Vec<(T::Var, Sort<T>)>,
166    pub out: Sort<T>,
167    pub body: Expr<T>,
168    #[derive_where(skip)]
169    pub comment: Option<String>,
170}
171
172#[derive_where(Hash)]
173pub struct Task<T: Types> {
174    #[derive_where(skip)]
175    pub comments: Vec<String>,
176    pub constants: Vec<ConstDecl<T>>,
177    pub data_decls: Vec<DataDecl<T>>,
178    pub define_funs: Vec<FunDef<T>>,
179    pub kvars: Vec<KVarDecl<T>>,
180    pub constraint: Constraint<T>,
181    pub qualifiers: Vec<Qualifier<T>>,
182    pub scrape_quals: bool,
183    pub solver: SmtSolver,
184}
185
186#[derive(Clone, Copy, Hash)]
187pub enum SmtSolver {
188    Z3,
189    CVC5,
190}
191
192impl fmt::Display for SmtSolver {
193    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
194        match self {
195            SmtSolver::Z3 => write!(f, "z3"),
196            SmtSolver::CVC5 => write!(f, "cvc5"),
197        }
198    }
199}
200
201#[derive(Serialize, Deserialize, Debug, Clone)]
202#[serde(
203    tag = "tag",
204    content = "contents",
205    bound(deserialize = "Tag: FromStr", serialize = "Tag: ToString")
206)]
207pub enum FixpointResult<Tag> {
208    Safe(Stats),
209    Unsafe(Stats, Vec<Error<Tag>>),
210    Crash(CrashInfo),
211}
212
213#[derive(Debug, Clone)]
214pub struct Error<Tag> {
215    pub id: i32,
216    pub tag: Tag,
217}
218
219#[derive(Debug, Serialize, Deserialize, Default, Clone)]
220#[serde(rename_all = "camelCase")]
221pub struct Stats {
222    pub num_cstr: i32,
223    pub num_iter: i32,
224    pub num_chck: i32,
225    pub num_vald: i32,
226}
227
228#[derive(Serialize, Deserialize, Debug, Clone)]
229pub struct CrashInfo(Vec<serde_json::Value>);
230
231#[derive_where(Debug, Clone, Hash)]
232pub struct KVarDecl<T: Types> {
233    pub kvid: T::KVar,
234    pub sorts: Vec<Sort<T>>,
235    #[derive_where(skip)]
236    pub comment: String,
237}
238
239impl<T: Types> Task<T> {
240    pub fn hash_with_default(&self) -> u64 {
241        let mut hasher = DefaultHasher::new();
242        self.hash(&mut hasher);
243        hasher.finish()
244    }
245
246    pub fn run(&self) -> io::Result<FixpointResult<T::Tag>> {
247        let mut child = Command::new("fixpoint")
248            .arg("-q")
249            .arg("--stdin")
250            .arg("--json")
251            .arg("--allowho")
252            .arg("--allowhoqs")
253            .arg(format!("--solver={}", self.solver))
254            .stdin(Stdio::piped())
255            .stdout(Stdio::piped())
256            .stderr(Stdio::piped())
257            .spawn()?;
258        let mut stdin = None;
259        std::mem::swap(&mut stdin, &mut child.stdin);
260        {
261            let mut w = BufWriter::new(stdin.unwrap());
262            writeln!(w, "{self}")?;
263        }
264        let out = child.wait_with_output()?;
265
266        serde_json::from_slice(&out.stdout).map_err(|err| {
267            // If we fail to parse stdout fixpoint may have outputed something to stderr
268            // so use that for the error instead
269            if !out.stderr.is_empty() {
270                let stderr = std::str::from_utf8(&out.stderr)
271                    .unwrap_or("fixpoint exited with a non-zero return code");
272                io::Error::other(stderr)
273            } else {
274                err.into()
275            }
276        })
277    }
278}
279
280impl<T: Types> KVarDecl<T> {
281    pub fn new(kvid: T::KVar, sorts: Vec<Sort<T>>, comment: String) -> Self {
282        Self { kvid, sorts, comment }
283    }
284}
285
286#[derive(Serialize, Deserialize)]
287struct ErrorInner(i32, String);
288
289impl<Tag: ToString> Serialize for Error<Tag> {
290    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
291    where
292        S: serde::Serializer,
293    {
294        ErrorInner(self.id, self.tag.to_string()).serialize(serializer)
295    }
296}
297
298impl<'de, Tag: FromStr> Deserialize<'de> for Error<Tag> {
299    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
300    where
301        D: serde::Deserializer<'de>,
302    {
303        let ErrorInner(id, tag) = Deserialize::deserialize(deserializer)?;
304        let tag = tag
305            .parse()
306            .map_err(|_| de::Error::invalid_value(de::Unexpected::Str(&tag), &"valid tag"))?;
307        Ok(Error { id, tag })
308    }
309}
310
311#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
312#[cfg_attr(feature = "nightly", derive(Encodable, Decodable))]
313pub enum ThyFunc {
314    // STRINGS
315    StrLen,
316
317    // BIT VECTORS
318    BvZeroExtend(u8),
319    BvSignExtend(u8),
320    IntToBv8,
321    Bv8ToInt,
322    IntToBv32,
323    Bv32ToInt,
324    IntToBv64,
325    Bv64ToInt,
326    BvUle,
327    BvSle,
328    BvUge,
329    BvSge,
330    BvUdiv,
331    BvSdiv,
332    BvSrem,
333    BvUrem,
334    BvLshr,
335    BvAshr,
336    BvAnd,
337    BvOr,
338    BvXor,
339    BvNot,
340    BvAdd,
341    BvNeg,
342    BvSub,
343    BvMul,
344    BvShl,
345    BvUgt,
346    BvSgt,
347    BvUlt,
348    BvSlt,
349
350    // SETS
351    /// Make an empty set
352    SetEmpty,
353    /// Make a singleton set
354    SetSng,
355    /// Set union
356    SetCup,
357    /// Set membership
358    SetMem,
359
360    // MAPS
361    /// Create a map where all keys point to a value
362    MapDefault,
363    /// Select a key in a map
364    MapSelect,
365    /// Store a key value pair in a map
366    MapStore,
367}
368
369impl ThyFunc {
370    pub const ALL: [ThyFunc; 37] = [
371        ThyFunc::StrLen,
372        ThyFunc::IntToBv8,
373        ThyFunc::Bv8ToInt,
374        ThyFunc::IntToBv32,
375        ThyFunc::Bv32ToInt,
376        ThyFunc::IntToBv64,
377        ThyFunc::Bv64ToInt,
378        ThyFunc::BvAdd,
379        ThyFunc::BvNeg,
380        ThyFunc::BvSub,
381        ThyFunc::BvShl,
382        ThyFunc::BvLshr,
383        ThyFunc::BvAshr,
384        ThyFunc::BvMul,
385        ThyFunc::BvUdiv,
386        ThyFunc::BvSdiv,
387        ThyFunc::BvUrem,
388        ThyFunc::BvSrem,
389        ThyFunc::BvAnd,
390        ThyFunc::BvOr,
391        ThyFunc::BvXor,
392        ThyFunc::BvNot,
393        ThyFunc::BvUle,
394        ThyFunc::BvSle,
395        ThyFunc::BvUge,
396        ThyFunc::BvSge,
397        ThyFunc::BvUgt,
398        ThyFunc::BvSgt,
399        ThyFunc::BvUlt,
400        ThyFunc::BvSlt,
401        ThyFunc::SetEmpty,
402        ThyFunc::SetSng,
403        ThyFunc::SetCup,
404        ThyFunc::SetMem,
405        ThyFunc::MapDefault,
406        ThyFunc::MapSelect,
407        ThyFunc::MapStore,
408    ];
409}
410
411impl fmt::Display for ThyFunc {
412    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
413        match self {
414            ThyFunc::StrLen => write!(f, "strLen"),
415            ThyFunc::BvZeroExtend(size) => {
416                // `app` is a hack in liquid-fixpoint used to implement indexed identifiers
417                write!(f, "app (_ zero_extend {size})")
418            }
419            ThyFunc::BvSignExtend(size) => write!(f, "app (_ sign_extend {size})"),
420            ThyFunc::IntToBv32 => write!(f, "int_to_bv32"),
421            ThyFunc::Bv32ToInt => write!(f, "bv32_to_int"),
422            ThyFunc::IntToBv8 => write!(f, "int_to_bv8"),
423            ThyFunc::Bv8ToInt => write!(f, "bv8_to_int"),
424            ThyFunc::IntToBv64 => write!(f, "int_to_bv64"),
425            ThyFunc::Bv64ToInt => write!(f, "bv64_to_int"),
426            ThyFunc::BvUle => write!(f, "bvule"),
427            ThyFunc::BvSle => write!(f, "bvsle"),
428            ThyFunc::BvUge => write!(f, "bvuge"),
429            ThyFunc::BvSge => write!(f, "bvsge"),
430            ThyFunc::BvUdiv => write!(f, "bvudiv"),
431            ThyFunc::BvSdiv => write!(f, "bvsdiv"),
432            ThyFunc::BvUrem => write!(f, "bvurem"),
433            ThyFunc::BvSrem => write!(f, "bvsrem"),
434            ThyFunc::BvLshr => write!(f, "bvlshr"),
435            ThyFunc::BvAshr => write!(f, "bvashr"),
436            ThyFunc::BvAnd => write!(f, "bvand"),
437            ThyFunc::BvOr => write!(f, "bvor"),
438            ThyFunc::BvXor => write!(f, "bvxor"),
439            ThyFunc::BvNot => write!(f, "bvnot"),
440            ThyFunc::BvAdd => write!(f, "bvadd"),
441            ThyFunc::BvNeg => write!(f, "bvneg"),
442            ThyFunc::BvSub => write!(f, "bvsub"),
443            ThyFunc::BvMul => write!(f, "bvmul"),
444            ThyFunc::BvShl => write!(f, "bvshl"),
445            ThyFunc::BvUgt => write!(f, "bvugt"),
446            ThyFunc::BvSgt => write!(f, "bvsgt"),
447            ThyFunc::BvUlt => write!(f, "bvult"),
448            ThyFunc::BvSlt => write!(f, "bvslt"),
449            ThyFunc::SetEmpty => write!(f, "Set_empty"),
450            ThyFunc::SetSng => write!(f, "Set_sng"),
451            ThyFunc::SetCup => write!(f, "Set_cup"),
452            ThyFunc::SetMem => write!(f, "Set_mem"),
453            ThyFunc::MapDefault => write!(f, "Map_default"),
454            ThyFunc::MapSelect => write!(f, "Map_select"),
455            ThyFunc::MapStore => write!(f, "Map_store"),
456        }
457    }
458}
liquid_fixpoint/lib.rs

liquid_fixpoint/
lib.rs
