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;
14mod format;
15
16use std::{
17    collections::hash_map::DefaultHasher,
18    fmt,
19    hash::{Hash, Hasher},
20    io::{self, BufWriter, Write as IOWrite},
21    process::{Command, Stdio},
22    str::FromStr,
23};
24
25pub use constraint::{
26    BinOp, BinRel, Bind, Constant, Constraint, DataCtor, DataDecl, DataField, Expr, Pred,
27    Qualifier, Sort, SortCtor,
28};
29use derive_where::derive_where;
30#[cfg(feature = "nightly")]
31use rustc_macros::{Decodable, Encodable};
32use serde::{Deserialize, Serialize, de};
33
34pub trait Types {
35    type Sort: Identifier + Hash + Clone;
36    type KVar: Identifier + Hash;
37    type Var: Identifier + Hash;
38    type Decimal: FixpointFmt + Hash;
39    type String: FixpointFmt + Hash;
40    type Tag: fmt::Display + FromStr + Hash;
41}
42
43pub trait FixpointFmt: Sized {
44    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result;
45
46    /// Returns a type that implements [`fmt::Display`] using this [`FixpointFmt::fmt`] implementation.
47    fn display(&self) -> impl fmt::Display {
48        struct DisplayAdapter<T>(T);
49        impl<T: FixpointFmt> std::fmt::Display for DisplayAdapter<&T> {
50            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
51                FixpointFmt::fmt(self.0, f)
52            }
53        }
54        DisplayAdapter(self)
55    }
56}
57
58pub trait Identifier: Sized {
59    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result;
60
61    /// Returns a type that implements [`fmt::Display`] using this [`Identifier::fmt`] implementation.
62    fn display(&self) -> impl fmt::Display {
63        struct DisplayAdapter<T>(T);
64        impl<T: Identifier> fmt::Display for DisplayAdapter<&T> {
65            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
66                Identifier::fmt(self.0, f)
67            }
68        }
69        DisplayAdapter(self)
70    }
71}
72
73struct DefaultTypes;
74
75impl Types for DefaultTypes {
76    type Sort = &'static str;
77    type KVar = &'static str;
78    type Var = &'static str;
79    type Tag = String;
80    type Decimal = u32;
81    type String = String;
82}
83
84impl Identifier for &str {
85    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
86        write!(f, "{self}")
87    }
88}
89
90impl FixpointFmt for u32 {
91    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
92        write!(f, "{self}")
93    }
94}
95
96impl FixpointFmt for String {
97    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
98        write!(f, "\"{self}\"")
99    }
100}
101
102#[macro_export]
103macro_rules! declare_types {
104    (   type Sort = $sort:ty;
105        type KVar = $kvar:ty;
106        type Var = $var:ty;
107        type Decimal = $real:ty;
108        type String = $str:ty;
109
110        type Tag = $tag:ty;
111    ) => {
112        pub mod fixpoint_generated {
113            pub struct FixpointTypes;
114            pub type Expr = $crate::Expr<FixpointTypes>;
115            pub type Pred = $crate::Pred<FixpointTypes>;
116            pub type Constraint = $crate::Constraint<FixpointTypes>;
117            pub type KVarDecl = $crate::KVarDecl<FixpointTypes>;
118            pub type ConstDecl = $crate::ConstDecl<FixpointTypes>;
119            pub type FunDef = $crate::FunDef<FixpointTypes>;
120            pub type Task = $crate::Task<FixpointTypes>;
121            pub type Qualifier = $crate::Qualifier<FixpointTypes>;
122            pub type Sort = $crate::Sort<FixpointTypes>;
123            pub type SortCtor = $crate::SortCtor<FixpointTypes>;
124            pub type DataDecl = $crate::DataDecl<FixpointTypes>;
125            pub type DataCtor = $crate::DataCtor<FixpointTypes>;
126            pub type DataField = $crate::DataField<FixpointTypes>;
127            pub type Bind = $crate::Bind<FixpointTypes>;
128            pub type Constant = $crate::Constant<FixpointTypes>;
129            pub use $crate::{BinOp, BinRel, ThyFunc};
130        }
131
132        impl $crate::Types for fixpoint_generated::FixpointTypes {
133            type Sort = $sort;
134            type KVar = $kvar;
135            type Var = $var;
136
137            type Decimal = $real;
138            type String = $str;
139
140            type Tag = $tag;
141        }
142    };
143}
144
145#[derive_where(Hash)]
146pub struct ConstDecl<T: Types> {
147    pub name: T::Var,
148    pub sort: Sort<T>,
149    #[derive_where(skip)]
150    pub comment: Option<String>,
151}
152
153#[derive_where(Hash)]
154pub struct FunDef<T: Types> {
155    pub name: T::Var,
156    pub args: Vec<(T::Var, Sort<T>)>,
157    pub out: Sort<T>,
158    pub body: Expr<T>,
159    #[derive_where(skip)]
160    pub comment: Option<String>,
161}
162
163#[derive_where(Hash)]
164pub struct Task<T: Types> {
165    #[derive_where(skip)]
166    pub comments: Vec<String>,
167    pub constants: Vec<ConstDecl<T>>,
168    pub data_decls: Vec<DataDecl<T>>,
169    pub define_funs: Vec<FunDef<T>>,
170    pub kvars: Vec<KVarDecl<T>>,
171    pub constraint: Constraint<T>,
172    pub qualifiers: Vec<Qualifier<T>>,
173    pub scrape_quals: bool,
174    pub solver: SmtSolver,
175}
176
177#[derive(Clone, Copy, Hash)]
178pub enum SmtSolver {
179    Z3,
180    CVC5,
181}
182
183impl fmt::Display for SmtSolver {
184    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
185        match self {
186            SmtSolver::Z3 => write!(f, "z3"),
187            SmtSolver::CVC5 => write!(f, "cvc5"),
188        }
189    }
190}
191
192#[derive(Serialize, Deserialize, Debug, Clone)]
193#[serde(
194    tag = "tag",
195    content = "contents",
196    bound(deserialize = "Tag: FromStr", serialize = "Tag: ToString")
197)]
198pub enum FixpointResult<Tag> {
199    Safe(Stats),
200    Unsafe(Stats, Vec<Error<Tag>>),
201    Crash(CrashInfo),
202}
203
204#[derive(Debug, Clone)]
205pub struct Error<Tag> {
206    pub id: i32,
207    pub tag: Tag,
208}
209
210#[derive(Debug, Serialize, Deserialize, Default, Clone)]
211#[serde(rename_all = "camelCase")]
212pub struct Stats {
213    pub num_cstr: i32,
214    pub num_iter: i32,
215    pub num_chck: i32,
216    pub num_vald: i32,
217}
218
219#[derive(Serialize, Deserialize, Debug, Clone)]
220pub struct CrashInfo(Vec<serde_json::Value>);
221
222#[derive_where(Hash)]
223pub struct KVarDecl<T: Types> {
224    kvid: T::KVar,
225    sorts: Vec<Sort<T>>,
226    #[derive_where(skip)]
227    comment: String,
228}
229
230impl<T: Types> Task<T> {
231    pub fn hash_with_default(&self) -> u64 {
232        let mut hasher = DefaultHasher::new();
233        self.hash(&mut hasher);
234        hasher.finish()
235    }
236
237    pub fn run(&self) -> io::Result<FixpointResult<T::Tag>> {
238        let mut child = Command::new("fixpoint")
239            .arg("-q")
240            .arg("--stdin")
241            .arg("--json")
242            .arg("--allowho")
243            .arg("--allowhoqs")
244            .arg(format!("--solver={}", self.solver))
245            .stdin(Stdio::piped())
246            .stdout(Stdio::piped())
247            .stderr(Stdio::piped())
248            .spawn()?;
249        let mut stdin = None;
250        std::mem::swap(&mut stdin, &mut child.stdin);
251        {
252            let mut w = BufWriter::new(stdin.unwrap());
253            writeln!(w, "{self}")?;
254        }
255        let out = child.wait_with_output()?;
256
257        serde_json::from_slice(&out.stdout).map_err(|err| {
258            // If we fail to parse stdout fixpoint may have outputed something to stderr
259            // so use that for the error instead
260            if !out.stderr.is_empty() {
261                let stderr = std::str::from_utf8(&out.stderr)
262                    .unwrap_or("fixpoint exited with a non-zero return code");
263                io::Error::new(io::ErrorKind::Other, stderr)
264            } else {
265                err.into()
266            }
267        })
268    }
269}
270
271impl<T: Types> KVarDecl<T> {
272    pub fn new(kvid: T::KVar, sorts: Vec<Sort<T>>, comment: String) -> Self {
273        Self { kvid, sorts, comment }
274    }
275}
276
277#[derive(Serialize, Deserialize)]
278struct ErrorInner(i32, String);
279
280impl<Tag: ToString> Serialize for Error<Tag> {
281    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
282    where
283        S: serde::Serializer,
284    {
285        ErrorInner(self.id, self.tag.to_string()).serialize(serializer)
286    }
287}
288
289impl<'de, Tag: FromStr> Deserialize<'de> for Error<Tag> {
290    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
291    where
292        D: serde::Deserializer<'de>,
293    {
294        let ErrorInner(id, tag) = Deserialize::deserialize(deserializer)?;
295        let tag = tag
296            .parse()
297            .map_err(|_| de::Error::invalid_value(de::Unexpected::Str(&tag), &"valid tag"))?;
298        Ok(Error { id, tag })
299    }
300}
301
302#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
303#[cfg_attr(feature = "nightly", derive(Encodable, Decodable))]
304pub enum ThyFunc {
305    // STRINGS
306    StrLen,
307
308    // BIT VECTORS
309    BvZeroExtend(u8),
310    BvSignExtend(u8),
311    IntToBv32,
312    Bv32ToInt,
313    IntToBv64,
314    Bv64ToInt,
315    BvUle,
316    BvSle,
317    BvUge,
318    BvSge,
319    BvUdiv,
320    BvSdiv,
321    BvSrem,
322    BvUrem,
323    BvLshr,
324    BvAshr,
325    BvAnd,
326    BvOr,
327    BvXor,
328    BvNot,
329    BvAdd,
330    BvNeg,
331    BvSub,
332    BvMul,
333    BvShl,
334    BvUgt,
335    BvSgt,
336    BvUlt,
337    BvSlt,
338
339    // SETS
340    /// Make an empty set
341    SetEmpty,
342    /// Make a singleton set
343    SetSng,
344    /// Set union
345    SetCup,
346    /// Set membership
347    SetMem,
348
349    // MAPS
350    /// Create a map where all keys point to a value
351    MapDefault,
352    /// Select a key in a map
353    MapSelect,
354    /// Store a key value pair in a map
355    MapStore,
356}
357
358impl ThyFunc {
359    pub const ALL: [ThyFunc; 35] = [
360        ThyFunc::StrLen,
361        ThyFunc::IntToBv32,
362        ThyFunc::Bv32ToInt,
363        ThyFunc::IntToBv64,
364        ThyFunc::Bv64ToInt,
365        ThyFunc::BvAdd,
366        ThyFunc::BvNeg,
367        ThyFunc::BvSub,
368        ThyFunc::BvShl,
369        ThyFunc::BvLshr,
370        ThyFunc::BvAshr,
371        ThyFunc::BvMul,
372        ThyFunc::BvUdiv,
373        ThyFunc::BvSdiv,
374        ThyFunc::BvUrem,
375        ThyFunc::BvSrem,
376        ThyFunc::BvAnd,
377        ThyFunc::BvOr,
378        ThyFunc::BvXor,
379        ThyFunc::BvNot,
380        ThyFunc::BvUle,
381        ThyFunc::BvSle,
382        ThyFunc::BvUge,
383        ThyFunc::BvSge,
384        ThyFunc::BvUgt,
385        ThyFunc::BvSgt,
386        ThyFunc::BvUlt,
387        ThyFunc::BvSlt,
388        ThyFunc::SetEmpty,
389        ThyFunc::SetSng,
390        ThyFunc::SetCup,
391        ThyFunc::SetMem,
392        ThyFunc::MapDefault,
393        ThyFunc::MapSelect,
394        ThyFunc::MapStore,
395    ];
396}
397
398impl fmt::Display for ThyFunc {
399    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
400        match self {
401            ThyFunc::StrLen => write!(f, "strLen"),
402            ThyFunc::BvZeroExtend(size) => {
403                // `app` is a hack in liquid-fixpoint used to implement indexed identifiers
404                write!(f, "app (_ zero_extend {size})")
405            }
406            ThyFunc::BvSignExtend(size) => write!(f, "app (_ sign_extend {size})"),
407            ThyFunc::IntToBv32 => write!(f, "int_to_bv32"),
408            ThyFunc::Bv32ToInt => write!(f, "bv32_to_int"),
409            ThyFunc::IntToBv64 => write!(f, "int_to_bv64"),
410            ThyFunc::Bv64ToInt => write!(f, "bv64_to_int"),
411            ThyFunc::BvUle => write!(f, "bvule"),
412            ThyFunc::BvSle => write!(f, "bvsle"),
413            ThyFunc::BvUge => write!(f, "bvuge"),
414            ThyFunc::BvSge => write!(f, "bvsge"),
415            ThyFunc::BvUdiv => write!(f, "bvudiv"),
416            ThyFunc::BvSdiv => write!(f, "bvsdiv"),
417            ThyFunc::BvUrem => write!(f, "bvurem"),
418            ThyFunc::BvSrem => write!(f, "bvsrem"),
419            ThyFunc::BvLshr => write!(f, "bvlshr"),
420            ThyFunc::BvAshr => write!(f, "bvashr"),
421            ThyFunc::BvAnd => write!(f, "bvand"),
422            ThyFunc::BvOr => write!(f, "bvor"),
423            ThyFunc::BvXor => write!(f, "bvxor"),
424            ThyFunc::BvNot => write!(f, "bvnot"),
425            ThyFunc::BvAdd => write!(f, "bvadd"),
426            ThyFunc::BvNeg => write!(f, "bvneg"),
427            ThyFunc::BvSub => write!(f, "bvsub"),
428            ThyFunc::BvMul => write!(f, "bvmul"),
429            ThyFunc::BvShl => write!(f, "bvshl"),
430            ThyFunc::BvUgt => write!(f, "bvugt"),
431            ThyFunc::BvSgt => write!(f, "bvsgt"),
432            ThyFunc::BvUlt => write!(f, "bvult"),
433            ThyFunc::BvSlt => write!(f, "bvslt"),
434            ThyFunc::SetEmpty => write!(f, "Set_empty"),
435            ThyFunc::SetSng => write!(f, "Set_sng"),
436            ThyFunc::SetCup => write!(f, "Set_cup"),
437            ThyFunc::SetMem => write!(f, "Set_mem"),
438            ThyFunc::MapDefault => write!(f, "Map_default"),
439            ThyFunc::MapSelect => write!(f, "Map_select"),
440            ThyFunc::MapStore => write!(f, "Map_store"),
441        }
442    }
443}
liquid_fixpoint/lib.rs

liquid_fixpoint/
lib.rs
