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

liquid_fixpoint/
lib.rs
