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

liquid_fixpoint/
lib.rs
