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

liquid_fixpoint/
lib.rs
