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

liquid_fixpoint/
lib.rs
