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("--sortedsolution")
337            .arg("--json")
338            .arg("--allowho")
339            .arg("--allowhoqs")
340            .arg(format!("--solver={}", self.solver))
341            .stdin(Stdio::piped())
342            .stdout(Stdio::piped())
343            .stderr(Stdio::piped())
344            .spawn()?;
345        let mut stdin = None;
346        std::mem::swap(&mut stdin, &mut child.stdin);
347        {
348            let mut w = BufWriter::new(stdin.unwrap());
349            writeln!(w, "{self}")?;
350        }
351        let out = child.wait_with_output()?;
352
353        serde_json::from_slice(&out.stdout).map_err(|err| {
354            // If we fail to parse stdout fixpoint may have outputed something to stderr
355            // so use that for the error instead
356            if !out.stderr.is_empty() {
357                let stderr = std::str::from_utf8(&out.stderr)
358                    .unwrap_or("fixpoint exited with a non-zero return code");
359                io::Error::other(stderr)
360            } else {
361                err.into()
362            }
363        })
364    }
365}
366
367impl<T: Types> KVarDecl<T> {
368    pub fn new(kvid: T::KVar, sorts: Vec<Sort<T>>, comment: String) -> Self {
369        Self { kvid, sorts, comment }
370    }
371}
372
373#[derive(Serialize, Deserialize)]
374struct ErrorInner(i32, String);
375
376impl<Tag: ToString> Serialize for Error<Tag> {
377    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
378    where
379        S: serde::Serializer,
380    {
381        ErrorInner(self.id, self.tag.to_string()).serialize(serializer)
382    }
383}
384
385impl<'de, Tag: FromStr> Deserialize<'de> for Error<Tag> {
386    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
387    where
388        D: serde::Deserializer<'de>,
389    {
390        let ErrorInner(id, tag) = Deserialize::deserialize(deserializer)?;
391        let tag = tag
392            .parse()
393            .map_err(|_| de::Error::invalid_value(de::Unexpected::Str(&tag), &"valid tag"))?;
394        Ok(Error { id, tag })
395    }
396}
397
398#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
399#[cfg_attr(feature = "nightly", derive(Encodable, Decodable))]
400pub enum ThyFunc {
401    // STRINGS
402    StrLen,
403    StrConcat,
404    StrPrefixOf,
405    StrSuffixOf,
406    StrContains,
407
408    // BIT VECTORS
409    BvZeroExtend(u8),
410    BvSignExtend(u8),
411    IntToBv8,
412    Bv8ToInt,
413    IntToBv32,
414    Bv32ToInt,
415    IntToBv64,
416    Bv64ToInt,
417    BvUle,
418    BvSle,
419    BvUge,
420    BvSge,
421    BvUdiv,
422    BvSdiv,
423    BvSrem,
424    BvUrem,
425    BvLshr,
426    BvAshr,
427    BvAnd,
428    BvOr,
429    BvXor,
430    BvNot,
431    BvAdd,
432    BvNeg,
433    BvSub,
434    BvMul,
435    BvShl,
436    BvUgt,
437    BvSgt,
438    BvUlt,
439    BvSlt,
440
441    // SETS
442    /// Make an empty set
443    SetEmpty,
444    /// Make a singleton set
445    SetSng,
446    /// Set union
447    SetCup,
448    /// Set intersection
449    SetCap,
450    /// Set difference
451    SetDif,
452    /// Subset
453    SetSub,
454    /// Set membership
455    SetMem,
456
457    // MAPS
458    /// Create a map where all keys point to a value
459    MapDefault,
460    /// Select a key in a map
461    MapSelect,
462    /// Store a key value pair in a map
463    MapStore,
464}
465
466impl ThyFunc {
467    pub const ALL: [ThyFunc; 44] = [
468        ThyFunc::StrLen,
469        ThyFunc::StrConcat,
470        ThyFunc::StrPrefixOf,
471        ThyFunc::StrSuffixOf,
472        ThyFunc::StrContains,
473        ThyFunc::IntToBv8,
474        ThyFunc::Bv8ToInt,
475        ThyFunc::IntToBv32,
476        ThyFunc::Bv32ToInt,
477        ThyFunc::IntToBv64,
478        ThyFunc::Bv64ToInt,
479        ThyFunc::BvAdd,
480        ThyFunc::BvNeg,
481        ThyFunc::BvSub,
482        ThyFunc::BvShl,
483        ThyFunc::BvLshr,
484        ThyFunc::BvAshr,
485        ThyFunc::BvMul,
486        ThyFunc::BvUdiv,
487        ThyFunc::BvSdiv,
488        ThyFunc::BvUrem,
489        ThyFunc::BvSrem,
490        ThyFunc::BvAnd,
491        ThyFunc::BvOr,
492        ThyFunc::BvXor,
493        ThyFunc::BvNot,
494        ThyFunc::BvUle,
495        ThyFunc::BvSle,
496        ThyFunc::BvUge,
497        ThyFunc::BvSge,
498        ThyFunc::BvUgt,
499        ThyFunc::BvSgt,
500        ThyFunc::BvUlt,
501        ThyFunc::BvSlt,
502        ThyFunc::SetEmpty,
503        ThyFunc::SetSng,
504        ThyFunc::SetCup,
505        ThyFunc::SetMem,
506        ThyFunc::SetCap,
507        ThyFunc::SetDif,
508        ThyFunc::SetSub,
509        ThyFunc::MapDefault,
510        ThyFunc::MapSelect,
511        ThyFunc::MapStore,
512    ];
513}
514
515impl fmt::Display for ThyFunc {
516    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
517        match self {
518            ThyFunc::StrLen => write!(f, "strLen"),
519            ThyFunc::StrConcat => write!(f, "strConcat"),
520            ThyFunc::StrPrefixOf => write!(f, "strPrefixOf"),
521            ThyFunc::StrSuffixOf => write!(f, "strSuffixOf"),
522            ThyFunc::StrContains => write!(f, "strContains"),
523            ThyFunc::BvZeroExtend(size) => {
524                // `app` is a hack in liquid-fixpoint used to implement indexed identifiers
525                write!(f, "app (_ zero_extend {size})")
526            }
527            ThyFunc::BvSignExtend(size) => write!(f, "app (_ sign_extend {size})"),
528            ThyFunc::IntToBv32 => write!(f, "int_to_bv32"),
529            ThyFunc::Bv32ToInt => write!(f, "bv32_to_int"),
530            ThyFunc::IntToBv8 => write!(f, "int_to_bv8"),
531            ThyFunc::Bv8ToInt => write!(f, "bv8_to_int"),
532            ThyFunc::IntToBv64 => write!(f, "int_to_bv64"),
533            ThyFunc::Bv64ToInt => write!(f, "bv64_to_int"),
534            ThyFunc::BvUle => write!(f, "bvule"),
535            ThyFunc::BvSle => write!(f, "bvsle"),
536            ThyFunc::BvUge => write!(f, "bvuge"),
537            ThyFunc::BvSge => write!(f, "bvsge"),
538            ThyFunc::BvUdiv => write!(f, "bvudiv"),
539            ThyFunc::BvSdiv => write!(f, "bvsdiv"),
540            ThyFunc::BvUrem => write!(f, "bvurem"),
541            ThyFunc::BvSrem => write!(f, "bvsrem"),
542            ThyFunc::BvLshr => write!(f, "bvlshr"),
543            ThyFunc::BvAshr => write!(f, "bvashr"),
544            ThyFunc::BvAnd => write!(f, "bvand"),
545            ThyFunc::BvOr => write!(f, "bvor"),
546            ThyFunc::BvXor => write!(f, "bvxor"),
547            ThyFunc::BvNot => write!(f, "bvnot"),
548            ThyFunc::BvAdd => write!(f, "bvadd"),
549            ThyFunc::BvNeg => write!(f, "bvneg"),
550            ThyFunc::BvSub => write!(f, "bvsub"),
551            ThyFunc::BvMul => write!(f, "bvmul"),
552            ThyFunc::BvShl => write!(f, "bvshl"),
553            ThyFunc::BvUgt => write!(f, "bvugt"),
554            ThyFunc::BvSgt => write!(f, "bvsgt"),
555            ThyFunc::BvUlt => write!(f, "bvult"),
556            ThyFunc::BvSlt => write!(f, "bvslt"),
557            ThyFunc::SetEmpty => write!(f, "Set_empty"),
558            ThyFunc::SetSng => write!(f, "Set_sng"),
559            ThyFunc::SetCup => write!(f, "Set_cup"),
560            ThyFunc::SetCap => write!(f, "Set_cap"),
561            ThyFunc::SetDif => write!(f, "Set_dif"),
562            ThyFunc::SetMem => write!(f, "Set_mem"),
563            ThyFunc::SetSub => write!(f, "Set_sub"),
564            ThyFunc::MapDefault => write!(f, "Map_default"),
565            ThyFunc::MapSelect => write!(f, "Map_select"),
566            ThyFunc::MapStore => write!(f, "Map_store"),
567        }
568    }
569}
liquid_fixpoint/lib.rs

liquid_fixpoint/
lib.rs
