z3tracer/
error.rs

1// Copyright (c) Facebook, Inc. and its affiliates
2// SPDX-License-Identifier: MIT OR Apache-2.0
3
4use crate::syntax::{Equality, Ident};
5
6/// Raw error cases.
7#[derive(Debug, Clone, Eq, PartialEq, thiserror::Error)]
8pub enum RawError {
9    // General
10    #[error("{0} {1} is not supported")]
11    UnsupportedVersion(String, String),
12    // Lexer
13    #[error("Invalid UTF8 string {0}")]
14    InvalidUtf8String(std::string::FromUtf8Error),
15    #[error("Invalid integer {0}")]
16    InvalidInteger(std::num::ParseIntError),
17    #[error("Invalid hexadecimal string {0}")]
18    InvalidHexadecimal(String),
19    #[error("Unexpected char or end of input: {0:?} instead of {1:?}")]
20    UnexpectedChar(Option<char>, Vec<char>),
21    #[error("Unexpected word: {0} instead of {1:?}")]
22    UnexpectedWord(String, Vec<&'static str>),
23    // Parser & Model
24    #[error("Missing identifier")]
25    MissingIdentifier,
26    #[error("Undefined identifier {0:?}")]
27    UndefinedIdent(Ident),
28    #[error("Unexpected proof term {0:?}")]
29    UnexpectedProofTerm(Ident),
30    #[error("Missing proof {0:?}")]
31    MissingProof(Ident),
32    #[error("Cannot attach meaning {0:?}")]
33    CannotAttachMeaning(Ident),
34    #[error("Cannot attach var name {0:?}")]
35    CannotAttachVarNames(Ident),
36    #[error("Unknown command {0}")]
37    UnknownCommand(String),
38    #[error("Invalid end of instance")]
39    InvalidEndOfInstance,
40    #[error("Invalid instance key")]
41    InvalidInstanceKey,
42    #[error("Invalid match key")]
43    InvalidMatchKey,
44    #[error("Cannot enode {0} {1}")]
45    CannotAttachEnode(usize, usize),
46    #[error("Cannot process equality {0:?} {1:?}")]
47    CannotProcessEquality(Ident, Equality),
48    #[error("Cannot check equality {0:?} {1:?}")]
49    CannotCheckEquality(Ident, Ident),
50    #[error("Invalid 'push' command {0}")]
51    InvalidPush(u64),
52    #[error("Invalid 'pop' command {0} {1}")]
53    InvalidPop(u64, u64),
54}
55
56/// Record a position in the input stream.
57#[derive(Clone, Eq, PartialEq, thiserror::Error)]
58#[error("{}{}:{}", match &.path_name { Some(p) => format!("{}:", p), None => String::new() }, .line + 1, .column + 1)]
59pub struct Position {
60    /// Optional path name for the input stream.
61    pub path_name: Option<String>,
62    /// Line number in the input stream.
63    pub line: usize,
64    /// Column number in the line.
65    pub column: usize,
66}
67
68/// An error together with a position where the error occurred.
69#[derive(Debug, Clone, Eq, PartialEq, thiserror::Error)]
70#[error("{position}: {error}")]
71pub struct Error {
72    pub position: Position,
73    pub error: RawError,
74}
75
76/// Result type based on `RawError`.
77pub type RawResult<T> = std::result::Result<T, RawError>;
78
79/// Result type based on `Error`.
80pub type Result<T> = std::result::Result<T, Error>;
81
82impl std::fmt::Debug for Position {
83    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
84        let file = match &self.path_name {
85            Some(p) => format!("{}:", p),
86            None => String::new(),
87        };
88        write!(f, "{}{}:{}", file, self.line + 1, self.column + 1)
89    }
90}
91
92const SUPPORTED_TOOL: &str = "Z3";
93const SUPPORTED_VERSIONS: &[&str] = &["4.8.9"];
94
95impl RawError {
96    pub fn check_that_tool_version_is_supported(s1: &str, s2: &str) -> RawResult<()> {
97        if s1 != SUPPORTED_TOOL || SUPPORTED_VERSIONS.iter().all(|x| s2 != *x) {
98            return Err(RawError::UnsupportedVersion(s1.to_string(), s2.to_string()));
99        }
100        Ok(())
101    }
102}
103
104impl From<Error> for RawError {
105    fn from(value: Error) -> Self {
106        value.error
107    }
108}
109
110#[test]
111fn test_version_check() {
112    assert!(RawError::check_that_tool_version_is_supported("Z3", "4.8.9").is_ok());
113    assert!(RawError::check_that_tool_version_is_supported("Z4", "4.8.9").is_err());
114    assert!(RawError::check_that_tool_version_is_supported("Z3", "4.8.10").is_err());
115}
z3tracer/error.rs

z3tracer/
error.rs
