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

liquid_fixpoint/
lib.rs
