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

liquid_fixpoint/
lib.rs
