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