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 FixpointStatus<Tag> {
204    Safe(Stats),
205    Unsafe(Stats, Vec<Error<Tag>>),
206    Crash(CrashInfo),
207}
208
209#[derive(Serialize, Deserialize, Debug, Clone)]
210#[serde(bound(deserialize = "Tag: FromStr", serialize = "Tag: ToString"))]
211pub struct FixpointResult<Tag> {
212    pub status: FixpointStatus<Tag>,
213}
214
215impl<Tag> FixpointStatus<Tag> {
216    pub fn is_safe(&self) -> bool {
217        matches!(self, FixpointStatus::Safe(_))
218    }
219
220    pub fn merge(self, other: FixpointStatus<Tag>) -> Self {
221        use FixpointStatus as FR;
222        match (self, other) {
223            (FR::Safe(stats1), FR::Safe(stats2)) => FR::Safe(stats1.merge(&stats2)),
224            (FR::Safe(stats1), FR::Unsafe(stats2, errors)) => {
225                FR::Unsafe(stats1.merge(&stats2), errors)
226            }
227            (FR::Unsafe(stats1, mut errors1), FR::Unsafe(stats2, errors2)) => {
228                errors1.extend(errors2);
229                FR::Unsafe(stats1.merge(&stats2), errors1)
230            }
231            (FR::Unsafe(stats1, errors), FR::Safe(stats2)) => {
232                FR::Unsafe(stats1.merge(&stats2), errors)
233            }
234            (FR::Crash(info1), FR::Crash(info2)) => FR::Crash(info1.merge(info2)),
235            (FR::Crash(info), _) => FR::Crash(info),
236            (_, FR::Crash(info)) => FR::Crash(info),
237        }
238    }
239}
240
241#[derive(Debug, Clone)]
242pub struct Error<Tag> {
243    pub id: i32,
244    pub tag: Tag,
245}
246
247#[derive(Debug, Serialize, Deserialize, Default, Clone)]
248#[serde(rename_all = "camelCase")]
249pub struct Stats {
250    pub num_cstr: i32,
251    pub num_iter: i32,
252    pub num_chck: i32,
253    pub num_vald: i32,
254}
255
256impl Stats {
257    pub fn merge(&self, other: &Stats) -> Self {
258        Stats {
259            num_cstr: self.num_cstr + other.num_cstr,
260            num_iter: self.num_iter + other.num_iter,
261            num_chck: self.num_chck + other.num_chck,
262            num_vald: self.num_vald + other.num_vald,
263        }
264    }
265}
266
267#[derive(Serialize, Deserialize, Debug, Clone)]
268pub struct CrashInfo(Vec<serde_json::Value>);
269
270impl CrashInfo {
271    pub fn merge(self, other: CrashInfo) -> Self {
272        let mut v = self.0;
273        v.extend(other.0);
274        CrashInfo(v)
275    }
276}
277
278#[derive_where(Debug, Clone, Hash)]
279pub struct KVarDecl<T: Types> {
280    pub kvid: T::KVar,
281    pub sorts: Vec<Sort<T>>,
282    #[derive_where(skip)]
283    pub comment: String,
284}
285
286impl<T: Types> Task<T> {
287    pub fn hash_with_default(&self) -> u64 {
288        let mut hasher = DefaultHasher::new();
289        self.hash(&mut hasher);
290        hasher.finish()
291    }
292
293    #[cfg(feature = "rust-fixpoint")]
294    pub fn run(&self) -> io::Result<FixpointResult<T::Tag>> {
295        let mut cstr_with_env = ConstraintWithEnv::new(
296            self.data_decls.clone(),
297            self.kvars.clone(),
298            self.qualifiers.clone(),
299            self.constants.clone(),
300            self.constraint.clone(),
301        );
302        Ok(FixpointResult { status: cstr_with_env.is_satisfiable() })
303    }
304
305    #[cfg(not(feature = "rust-fixpoint"))]
306    pub fn run(&self) -> io::Result<FixpointResult<T::Tag>> {
307        let mut child = Command::new("fixpoint")
308            .arg("-q")
309            .arg("--stdin")
310            .arg("--json")
311            .arg("--allowho")
312            .arg("--allowhoqs")
313            .arg(format!("--solver={}", self.solver))
314            .stdin(Stdio::piped())
315            .stdout(Stdio::piped())
316            .stderr(Stdio::piped())
317            .spawn()?;
318        let mut stdin = None;
319        std::mem::swap(&mut stdin, &mut child.stdin);
320        {
321            let mut w = BufWriter::new(stdin.unwrap());
322            writeln!(w, "{self}")?;
323        }
324        let out = child.wait_with_output()?;
325
326        serde_json::from_slice(&out.stdout).map_err(|err| {
327            // If we fail to parse stdout fixpoint may have outputed something to stderr
328            // so use that for the error instead
329            if !out.stderr.is_empty() {
330                let stderr = std::str::from_utf8(&out.stderr)
331                    .unwrap_or("fixpoint exited with a non-zero return code");
332                io::Error::other(stderr)
333            } else {
334                err.into()
335            }
336        })
337    }
338}
339
340impl<T: Types> KVarDecl<T> {
341    pub fn new(kvid: T::KVar, sorts: Vec<Sort<T>>, comment: String) -> Self {
342        Self { kvid, sorts, comment }
343    }
344}
345
346#[derive(Serialize, Deserialize)]
347struct ErrorInner(i32, String);
348
349impl<Tag: ToString> Serialize for Error<Tag> {
350    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
351    where
352        S: serde::Serializer,
353    {
354        ErrorInner(self.id, self.tag.to_string()).serialize(serializer)
355    }
356}
357
358impl<'de, Tag: FromStr> Deserialize<'de> for Error<Tag> {
359    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
360    where
361        D: serde::Deserializer<'de>,
362    {
363        let ErrorInner(id, tag) = Deserialize::deserialize(deserializer)?;
364        let tag = tag
365            .parse()
366            .map_err(|_| de::Error::invalid_value(de::Unexpected::Str(&tag), &"valid tag"))?;
367        Ok(Error { id, tag })
368    }
369}
370
371#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
372#[cfg_attr(feature = "nightly", derive(Encodable, Decodable))]
373pub enum ThyFunc {
374    // STRINGS
375    StrLen,
376
377    // BIT VECTORS
378    BvZeroExtend(u8),
379    BvSignExtend(u8),
380    IntToBv8,
381    Bv8ToInt,
382    IntToBv32,
383    Bv32ToInt,
384    IntToBv64,
385    Bv64ToInt,
386    BvUle,
387    BvSle,
388    BvUge,
389    BvSge,
390    BvUdiv,
391    BvSdiv,
392    BvSrem,
393    BvUrem,
394    BvLshr,
395    BvAshr,
396    BvAnd,
397    BvOr,
398    BvXor,
399    BvNot,
400    BvAdd,
401    BvNeg,
402    BvSub,
403    BvMul,
404    BvShl,
405    BvUgt,
406    BvSgt,
407    BvUlt,
408    BvSlt,
409
410    // SETS
411    /// Make an empty set
412    SetEmpty,
413    /// Make a singleton set
414    SetSng,
415    /// Set union
416    SetCup,
417    /// Set intersection
418    SetCap,
419    /// Set difference
420    SetDif,
421    /// Subset
422    SetSub,
423    /// Set membership
424    SetMem,
425
426    // MAPS
427    /// Create a map where all keys point to a value
428    MapDefault,
429    /// Select a key in a map
430    MapSelect,
431    /// Store a key value pair in a map
432    MapStore,
433}
434
435impl ThyFunc {
436    pub const ALL: [ThyFunc; 40] = [
437        ThyFunc::StrLen,
438        ThyFunc::IntToBv8,
439        ThyFunc::Bv8ToInt,
440        ThyFunc::IntToBv32,
441        ThyFunc::Bv32ToInt,
442        ThyFunc::IntToBv64,
443        ThyFunc::Bv64ToInt,
444        ThyFunc::BvAdd,
445        ThyFunc::BvNeg,
446        ThyFunc::BvSub,
447        ThyFunc::BvShl,
448        ThyFunc::BvLshr,
449        ThyFunc::BvAshr,
450        ThyFunc::BvMul,
451        ThyFunc::BvUdiv,
452        ThyFunc::BvSdiv,
453        ThyFunc::BvUrem,
454        ThyFunc::BvSrem,
455        ThyFunc::BvAnd,
456        ThyFunc::BvOr,
457        ThyFunc::BvXor,
458        ThyFunc::BvNot,
459        ThyFunc::BvUle,
460        ThyFunc::BvSle,
461        ThyFunc::BvUge,
462        ThyFunc::BvSge,
463        ThyFunc::BvUgt,
464        ThyFunc::BvSgt,
465        ThyFunc::BvUlt,
466        ThyFunc::BvSlt,
467        ThyFunc::SetEmpty,
468        ThyFunc::SetSng,
469        ThyFunc::SetCup,
470        ThyFunc::SetMem,
471        ThyFunc::SetCap,
472        ThyFunc::SetDif,
473        ThyFunc::SetSub,
474        ThyFunc::MapDefault,
475        ThyFunc::MapSelect,
476        ThyFunc::MapStore,
477    ];
478}
479
480impl fmt::Display for ThyFunc {
481    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
482        match self {
483            ThyFunc::StrLen => write!(f, "strLen"),
484            ThyFunc::BvZeroExtend(size) => {
485                // `app` is a hack in liquid-fixpoint used to implement indexed identifiers
486                write!(f, "app (_ zero_extend {size})")
487            }
488            ThyFunc::BvSignExtend(size) => write!(f, "app (_ sign_extend {size})"),
489            ThyFunc::IntToBv32 => write!(f, "int_to_bv32"),
490            ThyFunc::Bv32ToInt => write!(f, "bv32_to_int"),
491            ThyFunc::IntToBv8 => write!(f, "int_to_bv8"),
492            ThyFunc::Bv8ToInt => write!(f, "bv8_to_int"),
493            ThyFunc::IntToBv64 => write!(f, "int_to_bv64"),
494            ThyFunc::Bv64ToInt => write!(f, "bv64_to_int"),
495            ThyFunc::BvUle => write!(f, "bvule"),
496            ThyFunc::BvSle => write!(f, "bvsle"),
497            ThyFunc::BvUge => write!(f, "bvuge"),
498            ThyFunc::BvSge => write!(f, "bvsge"),
499            ThyFunc::BvUdiv => write!(f, "bvudiv"),
500            ThyFunc::BvSdiv => write!(f, "bvsdiv"),
501            ThyFunc::BvUrem => write!(f, "bvurem"),
502            ThyFunc::BvSrem => write!(f, "bvsrem"),
503            ThyFunc::BvLshr => write!(f, "bvlshr"),
504            ThyFunc::BvAshr => write!(f, "bvashr"),
505            ThyFunc::BvAnd => write!(f, "bvand"),
506            ThyFunc::BvOr => write!(f, "bvor"),
507            ThyFunc::BvXor => write!(f, "bvxor"),
508            ThyFunc::BvNot => write!(f, "bvnot"),
509            ThyFunc::BvAdd => write!(f, "bvadd"),
510            ThyFunc::BvNeg => write!(f, "bvneg"),
511            ThyFunc::BvSub => write!(f, "bvsub"),
512            ThyFunc::BvMul => write!(f, "bvmul"),
513            ThyFunc::BvShl => write!(f, "bvshl"),
514            ThyFunc::BvUgt => write!(f, "bvugt"),
515            ThyFunc::BvSgt => write!(f, "bvsgt"),
516            ThyFunc::BvUlt => write!(f, "bvult"),
517            ThyFunc::BvSlt => write!(f, "bvslt"),
518            ThyFunc::SetEmpty => write!(f, "Set_empty"),
519            ThyFunc::SetSng => write!(f, "Set_sng"),
520            ThyFunc::SetCup => write!(f, "Set_cup"),
521            ThyFunc::SetCap => write!(f, "Set_cap"),
522            ThyFunc::SetDif => write!(f, "Set_dif"),
523            ThyFunc::SetMem => write!(f, "Set_mem"),
524            ThyFunc::SetSub => write!(f, "Set_sub"),
525            ThyFunc::MapDefault => write!(f, "Map_default"),
526            ThyFunc::MapSelect => write!(f, "Map_select"),
527            ThyFunc::MapStore => write!(f, "Map_store"),
528        }
529    }
530}
liquid_fixpoint/lib.rs

liquid_fixpoint/
lib.rs
