Back to downloading of jars

modelator/Cargo.toml

@@ -14,6 +14,7 @@ sha2 = "0.9.3"
 thiserror = "1.0.24"
 tracing = "0.1.25"
 tracing-subscriber = "0.2.16"
+ureq = "2.1.0"
 
 # paste = "1.0"
 # seq-macro = "0.2.1"

modelator/src/artifact/tla_cfg_file.rs

@@ -1,4 +1,5 @@
 use crate::Error;
+use std::convert::TryFrom;
 use std::path::{Path, PathBuf};
 
 #[derive(Debug, Clone, PartialEq, Eq)]
@@ -7,27 +8,38 @@ pub struct TlaConfigFile {
 }
 
 impl TlaConfigFile {
-    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Self {
-        Self {
-            path: path.as_ref().to_path_buf(),
-        }
+    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Result<Self, Error> {
+        let path = path.as_ref().to_path_buf();
+        crate::util::check_file_existence(&path)?;
+        Ok(Self { path })
     }
 
     pub fn path(&self) -> &PathBuf {
         &self.path
     }
+}
+
+// TODO: replace the following `TryFrom` implementations with one with generic
+//       bound `AsRef<Path>` once https://github.com/rust-lang/rust/issues/50133
+//       is fixed
+impl TryFrom<String> for TlaConfigFile {
+    type Error = crate::Error;
+    fn try_from(path: String) -> Result<Self, Self::Error> {
+        Self::new(path)
+    }
+}
 
-    pub(crate) fn check_existence(&self) -> Result<(), Error> {
-        crate::util::check_file_existence(&self.path)
+impl TryFrom<&Path> for TlaConfigFile {
+    type Error = crate::Error;
+    fn try_from(path: &Path) -> Result<Self, Self::Error> {
+        Self::new(path)
     }
 }
 
-impl<P> From<P> for TlaConfigFile
-where
-    P: AsRef<Path>,
-{
-    fn from(path: P) -> Self {
-        Self::new(path.as_ref().to_path_buf())
+impl TryFrom<PathBuf> for TlaConfigFile {
+    type Error = crate::Error;
+    fn try_from(path: PathBuf) -> Result<Self, Self::Error> {
+        Self::new(path)
     }
 }
 

modelator/src/artifact/tla_file.rs

@@ -1,4 +1,5 @@
 use crate::Error;
+use std::convert::TryFrom;
 use std::path::{Path, PathBuf};
 
 #[derive(Debug, Clone, PartialEq, Eq)]
@@ -7,20 +8,16 @@ pub struct TlaFile {
 }
 
 impl TlaFile {
-    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Self {
-        Self {
-            path: path.as_ref().to_path_buf(),
-        }
+    pub(crate) fn new<P: AsRef<Path>>(path: P) -> Result<Self, Error> {
+        let path = path.as_ref().to_path_buf();
+        crate::util::check_file_existence(&path)?;
+        Ok(Self { path })
     }
 
     pub fn path(&self) -> &PathBuf {
         &self.path
     }
 
-    pub(crate) fn check_existence(&self) -> Result<(), Error> {
-        crate::util::check_file_existence(&self.path)
-    }
-
     /// Infer TLA module name. We assume that the TLA module name matches the
     /// name of the file.
     pub(crate) fn tla_module_name(&self) -> Option<String> {
@@ -37,12 +34,27 @@ impl TlaFile {
     }
 }
 
-impl<P> From<P> for TlaFile
-where
-    P: AsRef<Path>,
-{
-    fn from(path: P) -> Self {
-        Self::new(path.as_ref().to_path_buf())
+// TODO: replace the following `TryFrom` implementations with one with generic
+//       bound `AsRef<Path>` once https://github.com/rust-lang/rust/issues/50133
+//       is fixed
+impl TryFrom<String> for TlaFile {
+    type Error = crate::Error;
+    fn try_from(path: String) -> Result<Self, Self::Error> {
+        Self::new(path)
+    }
+}
+
+impl TryFrom<&Path> for TlaFile {
+    type Error = crate::Error;
+    fn try_from(path: &Path) -> Result<Self, Self::Error> {
+        Self::new(path)
+    }
+}
+
+impl TryFrom<PathBuf> for TlaFile {
+    type Error = crate::Error;
+    fn try_from(path: PathBuf) -> Result<Self, Self::Error> {
+        Self::new(path)
     }
 }
 

modelator/src/cache/tla_trace.rs

@@ -1,8 +1,6 @@
 use super::Cache;
 use crate::artifact::{TlaConfigFile, TlaFile, TlaTrace};
 use crate::{Error, Options};
-use sha2::Digest;
-use std::collections::BTreeSet;
 
 pub(crate) struct TlaTraceCache {
     cache: Cache,
@@ -46,41 +44,17 @@ impl TlaTraceCache {
             .collect();
 
         tracing::debug!("files to hash: {:?}", files_to_hash);
-        let mut digest = hash_files(files_to_hash)?;
+        let mut digest = crate::util::digest::digest_files(files_to_hash)?;
 
         // also add the absolute path of the tla file to the digest; this makes
         // sure that two tla tests files living in the same directory and using
         // the same tla configuration (which we shouldn't happen when using
         // `modelator::module::tla::generate_tests`) will have different hashes
+        use sha2::Digest;
         digest.update(&crate::util::absolute_path(&tla_file.path()));
 
-        let hash = hex::encode(digest.finalize());
+        let hash = crate::util::digest::encode(digest);
         tracing::debug!("computed hash: {}", hash);
         Ok(hash)
     }
 }
-
-fn hash_files(paths: BTreeSet<String>) -> Result<sha2::Sha256, Error> {
-    let mut digest = sha2::Sha256::default();
-    for path in paths {
-        hash_file(path, &mut digest)?;
-    }
-    Ok(digest)
-}
-
-fn hash_file(path: String, digest: &mut sha2::Sha256) -> Result<(), Error> {
-    let file = std::fs::File::open(path).map_err(Error::io)?;
-    let mut reader = std::io::BufReader::new(file);
-
-    let mut buffer = [0; 1024];
-    loop {
-        use std::io::Read;
-        let count = reader.read(&mut buffer).map_err(Error::io)?;
-        if count == 0 {
-            break;
-        }
-        digest.update(&buffer[..count]);
-    }
-
-    Ok(())
-}

modelator/src/cli/mod.rs

@@ -55,6 +55,11 @@ pub enum ApalacheMethods {
         /// TLA+ config file generated by the generate-test method in the TLA module.
         tla_config_file: String,
     },
+    /// Parse a TLA+ file.
+    Parse {
+        /// TLA+ file to be parsed.
+        tla_file: String,
+    },
 }
 
 #[derive(Debug, Clap)]
@@ -105,7 +110,10 @@ impl TlaMethods {
     }
 
     fn generate_tests(tla_file: String, tla_config_file: String) -> Result<JsonValue, Error> {
-        let tests = crate::module::Tla::generate_tests(tla_file.into(), tla_config_file.into())?;
+        use std::convert::TryFrom;
+        let tla_file = TlaFile::try_from(tla_file)?;
+        let tla_config_file = TlaConfigFile::try_from(tla_config_file)?;
+        let tests = crate::module::Tla::generate_tests(tla_file, tla_config_file)?;
         tracing::debug!("Tla::generate_tests output {:#?}", tests);
 
         generated_tests(tests)
@@ -135,17 +143,30 @@ impl ApalacheMethods {
                 tla_file,
                 tla_config_file,
             } => Self::test(tla_file, tla_config_file),
+            Self::Parse { tla_file } => Self::parse(tla_file),
         }
     }
 
     fn test(tla_file: String, tla_config_file: String) -> Result<JsonValue, Error> {
         let options = crate::Options::default();
-        let tla_trace =
-            crate::module::Apalache::test(tla_file.into(), tla_config_file.into(), &options)?;
+        use std::convert::TryFrom;
+        let tla_file = TlaFile::try_from(tla_file)?;
+        let tla_config_file = TlaConfigFile::try_from(tla_config_file)?;
+        let tla_trace = crate::module::Apalache::test(tla_file, tla_config_file, &options)?;
         tracing::debug!("Apalache::test output {}", tla_trace);
 
         save_tla_trace(tla_trace)
     }
+
+    fn parse(tla_file: String) -> Result<JsonValue, Error> {
+        let options = crate::Options::default();
+        use std::convert::TryFrom;
+        let tla_file = TlaFile::try_from(tla_file)?;
+        let tla_file_parsed = crate::module::Apalache::parse(tla_file, &options)?;
+        tracing::debug!("Apalache::parse output {}", tla_file_parsed);
+
+        parsed_tla_file(tla_file_parsed)
+    }
 }
 
 impl TlcMethods {
@@ -160,8 +181,10 @@ impl TlcMethods {
 
     fn test(tla_file: String, tla_config_file: String) -> Result<JsonValue, Error> {
         let options = crate::Options::default();
-        let tla_trace =
-            crate::module::Tlc::test(tla_file.into(), tla_config_file.into(), &options)?;
+        use std::convert::TryFrom;
+        let tla_file = TlaFile::try_from(tla_file)?;
+        let tla_config_file = TlaConfigFile::try_from(tla_config_file)?;
+        let tla_trace = crate::module::Tlc::test(tla_file, tla_config_file, &options)?;
         tracing::debug!("Tlc::test output {}", tla_trace);
 
         save_tla_trace(tla_trace)
@@ -198,3 +221,10 @@ fn save_json_trace(json_trace: JsonTrace) -> Result<JsonValue, Error> {
         "json_trace_file": crate::util::absolute_path(&path),
     }))
 }
+
+#[allow(clippy::unnecessary_wraps)]
+fn parsed_tla_file(tla_file_parsed: TlaFile) -> Result<JsonValue, Error> {
+    Ok(json!({
+        "tla_file": format!("{}", tla_file_parsed),
+    }))
+}

modelator/src/error.rs

@@ -41,6 +41,9 @@ pub enum Error {
     #[error("Invalid Apalache counterexample: {0}")]
     InvalidApalacheCounterexample(String),
 
+    #[error("Ureq error: {0}")]
+    Ureq(String),
+
     #[error("Nom error: {0}")]
     Nom(String),
 }
@@ -50,6 +53,10 @@ impl Error {
         Error::IO(err.to_string())
     }
 
+    pub(crate) fn ureq(err: ureq::Error) -> Error {
+        Error::Ureq(err.to_string())
+    }
+
     pub(crate) fn nom(err: nom::Err<nom::error::Error<&str>>) -> Error {
         Error::Nom(err.to_string())
     }