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

liquid_fixpoint/
lib.rs
