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 FixpointResult<Tag> {
204 Safe(Stats),
205 Unsafe(Stats, Vec<Error<Tag>>),
206 Crash(CrashInfo),
207}
208
209impl<Tag> FixpointResult<Tag> {
210 pub fn is_safe(&self) -> bool {
211 matches!(self, FixpointResult::Safe(_))
212 }
213
214 pub fn merge(self, other: FixpointResult<Tag>) -> Self {
215 use FixpointResult as FR;
216 match (self, other) {
217 (FR::Safe(stats1), FR::Safe(stats2)) => FR::Safe(stats1.merge(&stats2)),
218 (FR::Safe(stats1), FR::Unsafe(stats2, errors)) => {
219 FR::Unsafe(stats1.merge(&stats2), errors)
220 }
221 (FR::Unsafe(stats1, mut errors1), FR::Unsafe(stats2, errors2)) => {
222 errors1.extend(errors2);
223 FR::Unsafe(stats1.merge(&stats2), errors1)
224 }
225 (FR::Unsafe(stats1, errors), FR::Safe(stats2)) => {
226 FR::Unsafe(stats1.merge(&stats2), errors)
227 }
228 (FR::Crash(info1), FR::Crash(info2)) => FR::Crash(info1.merge(info2)),
229 (FR::Crash(info), _) => FR::Crash(info),
230 (_, FR::Crash(info)) => FR::Crash(info),
231 }
232 }
233}
234
235#[derive(Debug, Clone)]
236pub struct Error<Tag> {
237 pub id: i32,
238 pub tag: Tag,
239}
240
241#[derive(Debug, Serialize, Deserialize, Default, Clone)]
242#[serde(rename_all = "camelCase")]
243pub struct Stats {
244 pub num_cstr: i32,
245 pub num_iter: i32,
246 pub num_chck: i32,
247 pub num_vald: i32,
248}
249
250impl Stats {
251 pub fn merge(&self, other: &Stats) -> Self {
252 Stats {
253 num_cstr: self.num_cstr + other.num_cstr,
254 num_iter: self.num_iter + other.num_iter,
255 num_chck: self.num_chck + other.num_chck,
256 num_vald: self.num_vald + other.num_vald,
257 }
258 }
259}
260
261#[derive(Serialize, Deserialize, Debug, Clone)]
262pub struct CrashInfo(Vec<serde_json::Value>);
263
264impl CrashInfo {
265 pub fn merge(self, other: CrashInfo) -> Self {
266 let mut v = self.0;
267 v.extend(other.0);
268 CrashInfo(v)
269 }
270}
271
272#[derive_where(Debug, Clone, Hash)]
273pub struct KVarDecl<T: Types> {
274 pub kvid: T::KVar,
275 pub sorts: Vec<Sort<T>>,
276 #[derive_where(skip)]
277 pub comment: String,
278}
279
280impl<T: Types> Task<T> {
281 pub fn hash_with_default(&self) -> u64 {
282 let mut hasher = DefaultHasher::new();
283 self.hash(&mut hasher);
284 hasher.finish()
285 }
286
287 #[cfg(feature = "rust-fixpoint")]
288 pub fn run(&self) -> io::Result<FixpointResult<T::Tag>> {
289 let mut cstr_with_env = ConstraintWithEnv::new(
290 self.data_decls.clone(),
291 self.kvars.clone(),
292 self.qualifiers.clone(),
293 self.constants.clone(),
294 self.constraint.clone(),
295 );
296 let is_satisfiable = cstr_with_env.is_satisfiable();
297 Ok(is_satisfiable)
298 }
299
300 #[cfg(not(feature = "rust-fixpoint"))]
301 pub fn run(&self) -> io::Result<FixpointResult<T::Tag>> {
302 let mut child = Command::new("fixpoint")
303 .arg("-q")
304 .arg("--stdin")
305 .arg("--json")
306 .arg("--allowho")
307 .arg("--allowhoqs")
308 .arg(format!("--solver={}", self.solver))
309 .stdin(Stdio::piped())
310 .stdout(Stdio::piped())
311 .stderr(Stdio::piped())
312 .spawn()?;
313 let mut stdin = None;
314 std::mem::swap(&mut stdin, &mut child.stdin);
315 {
316 let mut w = BufWriter::new(stdin.unwrap());
317 writeln!(w, "{self}")?;
318 }
319 let out = child.wait_with_output()?;
320
321 serde_json::from_slice(&out.stdout).map_err(|err| {
322 if !out.stderr.is_empty() {
325 let stderr = std::str::from_utf8(&out.stderr)
326 .unwrap_or("fixpoint exited with a non-zero return code");
327 io::Error::other(stderr)
328 } else {
329 err.into()
330 }
331 })
332 }
333}
334
335impl<T: Types> KVarDecl<T> {
336 pub fn new(kvid: T::KVar, sorts: Vec<Sort<T>>, comment: String) -> Self {
337 Self { kvid, sorts, comment }
338 }
339}
340
341#[derive(Serialize, Deserialize)]
342struct ErrorInner(i32, String);
343
344impl<Tag: ToString> Serialize for Error<Tag> {
345 fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
346 where
347 S: serde::Serializer,
348 {
349 ErrorInner(self.id, self.tag.to_string()).serialize(serializer)
350 }
351}
352
353impl<'de, Tag: FromStr> Deserialize<'de> for Error<Tag> {
354 fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
355 where
356 D: serde::Deserializer<'de>,
357 {
358 let ErrorInner(id, tag) = Deserialize::deserialize(deserializer)?;
359 let tag = tag
360 .parse()
361 .map_err(|_| de::Error::invalid_value(de::Unexpected::Str(&tag), &"valid tag"))?;
362 Ok(Error { id, tag })
363 }
364}
365
366#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
367#[cfg_attr(feature = "nightly", derive(Encodable, Decodable))]
368pub enum ThyFunc {
369 StrLen,
371
372 BvZeroExtend(u8),
374 BvSignExtend(u8),
375 IntToBv8,
376 Bv8ToInt,
377 IntToBv32,
378 Bv32ToInt,
379 IntToBv64,
380 Bv64ToInt,
381 BvUle,
382 BvSle,
383 BvUge,
384 BvSge,
385 BvUdiv,
386 BvSdiv,
387 BvSrem,
388 BvUrem,
389 BvLshr,
390 BvAshr,
391 BvAnd,
392 BvOr,
393 BvXor,
394 BvNot,
395 BvAdd,
396 BvNeg,
397 BvSub,
398 BvMul,
399 BvShl,
400 BvUgt,
401 BvSgt,
402 BvUlt,
403 BvSlt,
404
405 SetEmpty,
408 SetSng,
410 SetCup,
412 SetCap,
414 SetDif,
416 SetSub,
418 SetMem,
420
421 MapDefault,
424 MapSelect,
426 MapStore,
428}
429
430impl ThyFunc {
431 pub const ALL: [ThyFunc; 40] = [
432 ThyFunc::StrLen,
433 ThyFunc::IntToBv8,
434 ThyFunc::Bv8ToInt,
435 ThyFunc::IntToBv32,
436 ThyFunc::Bv32ToInt,
437 ThyFunc::IntToBv64,
438 ThyFunc::Bv64ToInt,
439 ThyFunc::BvAdd,
440 ThyFunc::BvNeg,
441 ThyFunc::BvSub,
442 ThyFunc::BvShl,
443 ThyFunc::BvLshr,
444 ThyFunc::BvAshr,
445 ThyFunc::BvMul,
446 ThyFunc::BvUdiv,
447 ThyFunc::BvSdiv,
448 ThyFunc::BvUrem,
449 ThyFunc::BvSrem,
450 ThyFunc::BvAnd,
451 ThyFunc::BvOr,
452 ThyFunc::BvXor,
453 ThyFunc::BvNot,
454 ThyFunc::BvUle,
455 ThyFunc::BvSle,
456 ThyFunc::BvUge,
457 ThyFunc::BvSge,
458 ThyFunc::BvUgt,
459 ThyFunc::BvSgt,
460 ThyFunc::BvUlt,
461 ThyFunc::BvSlt,
462 ThyFunc::SetEmpty,
463 ThyFunc::SetSng,
464 ThyFunc::SetCup,
465 ThyFunc::SetMem,
466 ThyFunc::SetCap,
467 ThyFunc::SetDif,
468 ThyFunc::SetSub,
469 ThyFunc::MapDefault,
470 ThyFunc::MapSelect,
471 ThyFunc::MapStore,
472 ];
473}
474
475impl fmt::Display for ThyFunc {
476 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
477 match self {
478 ThyFunc::StrLen => write!(f, "strLen"),
479 ThyFunc::BvZeroExtend(size) => {
480 write!(f, "app (_ zero_extend {size})")
482 }
483 ThyFunc::BvSignExtend(size) => write!(f, "app (_ sign_extend {size})"),
484 ThyFunc::IntToBv32 => write!(f, "int_to_bv32"),
485 ThyFunc::Bv32ToInt => write!(f, "bv32_to_int"),
486 ThyFunc::IntToBv8 => write!(f, "int_to_bv8"),
487 ThyFunc::Bv8ToInt => write!(f, "bv8_to_int"),
488 ThyFunc::IntToBv64 => write!(f, "int_to_bv64"),
489 ThyFunc::Bv64ToInt => write!(f, "bv64_to_int"),
490 ThyFunc::BvUle => write!(f, "bvule"),
491 ThyFunc::BvSle => write!(f, "bvsle"),
492 ThyFunc::BvUge => write!(f, "bvuge"),
493 ThyFunc::BvSge => write!(f, "bvsge"),
494 ThyFunc::BvUdiv => write!(f, "bvudiv"),
495 ThyFunc::BvSdiv => write!(f, "bvsdiv"),
496 ThyFunc::BvUrem => write!(f, "bvurem"),
497 ThyFunc::BvSrem => write!(f, "bvsrem"),
498 ThyFunc::BvLshr => write!(f, "bvlshr"),
499 ThyFunc::BvAshr => write!(f, "bvashr"),
500 ThyFunc::BvAnd => write!(f, "bvand"),
501 ThyFunc::BvOr => write!(f, "bvor"),
502 ThyFunc::BvXor => write!(f, "bvxor"),
503 ThyFunc::BvNot => write!(f, "bvnot"),
504 ThyFunc::BvAdd => write!(f, "bvadd"),
505 ThyFunc::BvNeg => write!(f, "bvneg"),
506 ThyFunc::BvSub => write!(f, "bvsub"),
507 ThyFunc::BvMul => write!(f, "bvmul"),
508 ThyFunc::BvShl => write!(f, "bvshl"),
509 ThyFunc::BvUgt => write!(f, "bvugt"),
510 ThyFunc::BvSgt => write!(f, "bvsgt"),
511 ThyFunc::BvUlt => write!(f, "bvult"),
512 ThyFunc::BvSlt => write!(f, "bvslt"),
513 ThyFunc::SetEmpty => write!(f, "Set_empty"),
514 ThyFunc::SetSng => write!(f, "Set_sng"),
515 ThyFunc::SetCup => write!(f, "Set_cup"),
516 ThyFunc::SetCap => write!(f, "Set_cap"),
517 ThyFunc::SetDif => write!(f, "Set_dif"),
518 ThyFunc::SetMem => write!(f, "Set_mem"),
519 ThyFunc::SetSub => write!(f, "Set_sub"),
520 ThyFunc::MapDefault => write!(f, "Map_default"),
521 ThyFunc::MapSelect => write!(f, "Map_select"),
522 ThyFunc::MapStore => write!(f, "Map_store"),
523 }
524 }
525}