Add Souffle variants of some Algorithms

Author: ecstatic-morse

polonius-engine/src/lib.rs

@@ -13,4 +13,5 @@ pub use facts::AllFacts;
 pub use facts::Atom;
 pub use facts::FactTypes;
 pub use output::Algorithm;
+pub use output::Engine;
 pub use output::Output;

polonius-engine/src/output/mod.rs

@@ -21,13 +21,19 @@ mod liveness;
 mod location_insensitive;
 mod naive;
 
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum Engine {
+    Souffle,
+    Datafrog,
+}
+
 #[derive(Debug, Clone, Copy)]
 pub enum Algorithm {
     /// Simple rules, but slower to execute
-    Naive,
+    Naive(Engine),
 
     /// Optimized variant of the rules
-    DatafrogOpt,
+    DatafrogOpt(Engine),
 
     /// Fast to compute, but imprecise: there can be false-positives
     /// but no false-negatives. Tailored for quick "early return" situations.
@@ -42,14 +48,20 @@ pub enum Algorithm {
     Hybrid,
 }
 
+impl Default for Algorithm {
+    fn default() -> Self {
+        Self::Naive(Engine::Datafrog)
+    }
+}
+
 impl Algorithm {
     /// Optimized variants that ought to be equivalent to "naive"
-    pub const OPTIMIZED: &'static [Algorithm] = &[Algorithm::DatafrogOpt];
+    pub const OPTIMIZED: &'static [Algorithm] = &[Algorithm::DatafrogOpt(Engine::Datafrog)];
 
     pub fn variants() -> [&'static str; 5] {
         [
-            "Naive",
-            "DatafrogOpt",
+            "Naive(-Souffle)",
+            "DatafrogOpt(-Souffle)",
             "LocationInsensitive",
             "Compare",
             "Hybrid",
@@ -79,14 +91,14 @@ impl ::std::str::FromStr for Algorithm {
     type Err = String;
     fn from_str(s: &str) -> Result<Self, Self::Err> {
         match s.to_lowercase().as_ref() {
-            "naive" => Ok(Algorithm::Naive),
-            "datafrogopt" => Ok(Algorithm::DatafrogOpt),
+            "naive" => Ok(Algorithm::Naive(Engine::Datafrog)),
+            "naive-souffle" => Ok(Algorithm::Naive(Engine::Souffle)),
+            "datafrogopt" => Ok(Algorithm::DatafrogOpt(Engine::Datafrog)),
+            "datafrogopt-souffle" => Ok(Algorithm::DatafrogOpt(Engine::Souffle)),
             "locationinsensitive" => Ok(Algorithm::LocationInsensitive),
             "compare" => Ok(Algorithm::Compare),
             "hybrid" => Ok(Algorithm::Hybrid),
-            _ => Err(String::from(
-                "valid values: Naive, DatafrogOpt, LocationInsensitive, Compare, Hybrid",
-            )),
+            _ => Err(format!("valid values: {}", Self::variants().join(", "))),
         }
     }
 }
@@ -175,6 +187,29 @@ impl<T: FactTypes> Output<T> {
     ///   partial results can also be stored in the context, so that the following
     ///   variant can use it to prune its own input data
     pub fn compute(all_facts: &AllFacts<T>, algorithm: Algorithm, dump_enabled: bool) -> Self {
+        if algorithm.engine() == Engine::Souffle {
+            let name = algorithm.souffle_name().expect("Algorithm does not have Soufflé version");
+            let facts = polonius_souffle::run_from_facts(name, &all_facts);
+
+            let mut out = Output::new(dump_enabled);
+
+            for tuple in facts.get("errors").unwrap().iter() {
+                let [loan, location]: [u32; 2] = tuple.try_into().unwrap();
+                out.errors.entry(T::Point::from(location)).or_default().push(T::Loan::from(loan));
+            }
+
+            for tuple in facts.get("subset_errors").unwrap().iter()  {
+                let [origin1, origin2, location]: [u32; 3] = tuple.try_into().unwrap();
+                out
+                    .subset_errors
+                    .entry(T::Point::from(location))
+                    .or_default()
+                    .insert((T::Origin::from(origin1), T::Origin::from(origin2)));
+            }
+
+            return out;
+        }
+
         let mut result = Output::new(dump_enabled);
 
         // TODO: remove all the cloning thereafter, but that needs to be done in concert with rustc
@@ -317,8 +352,8 @@ impl<T: FactTypes> Output<T> {
 
                 (potential_errors, potential_subset_errors)
             }
-            Algorithm::Naive => naive::compute(&ctx, &mut result),
-            Algorithm::DatafrogOpt => datafrog_opt::compute(&ctx, &mut result),
+            Algorithm::Naive(_) => naive::compute(&ctx, &mut result),
+            Algorithm::DatafrogOpt(_) => datafrog_opt::compute(&ctx, &mut result),
             Algorithm::Hybrid => {
                 // Execute the fast `LocationInsensitive` computation as a pre-pass:
                 // if it finds no possible errors, we don't need to do the more complex

src/cli.rs

@@ -1,6 +1,6 @@
 use log::{error, Level, LevelFilter, Metadata, Record, SetLoggerError};
 use pico_args as pico;
-use polonius_engine::Algorithm;
+use polonius_engine::{Algorithm, Engine};
 use std::env;
 use std::error;
 use std::fmt;

src/test.rs

@@ -9,13 +9,13 @@ use crate::test_util::{
     assert_checkers_match, assert_equal, assert_outputs_match, location_insensitive_checker_for,
     naive_checker_for, opt_checker_for,
 };
-use polonius_engine::Algorithm;
+use polonius_engine::{Algorithm, Engine};
 use rustc_hash::FxHashMap;
 use std::error::Error;
 use std::path::Path;
 
 fn test_facts(all_facts: &AllFacts, algorithms: &[Algorithm]) {
-    let naive = Output::compute(all_facts, Algorithm::Naive, true);
+    let naive = Output::compute(all_facts, Algorithm::Naive(Engine::Datafrog), true);
 
     // Check that the "naive errors" are a subset of the "insensitive
     // ones".
@@ -111,7 +111,7 @@ macro_rules! tests {
 
                 #[test]
                 fn datafrog_opt() -> Result<(), Box<dyn Error>> {
-                    test_fn($dir, $fn, Algorithm::DatafrogOpt)
+                    test_fn($dir, $fn, Algorithm::DatafrogOpt(Engine::Datafrog))
                 }
             }
         )*
@@ -168,7 +168,7 @@ fn test_sensitive_passes_issue_47680() -> Result<(), Box<dyn Error>> {
         .join("main");
     let tables = &mut intern::InternerTables::new();
     let all_facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir)?;
-    let sensitive = Output::compute(&all_facts, Algorithm::DatafrogOpt, false);
+    let sensitive = Output::compute(&all_facts, Algorithm::DatafrogOpt(Engine::Datafrog), false);
 
     assert!(sensitive.errors.is_empty());
 
@@ -201,15 +201,15 @@ fn no_subset_symmetries_exist() -> Result<(), Box<dyn Error>> {
         false
     };
 
-    let naive = Output::compute(&all_facts, Algorithm::Naive, true);
+    let naive = Output::compute(&all_facts, Algorithm::Naive(Engine::Datafrog), true);
     assert!(!subset_symmetries_exist(&naive));
 
     // FIXME: the issue-47680 dataset is suboptimal here as DatafrogOpt does not
     // produce subset symmetries for it. It does for clap, and it was used to manually verify
     // that the assert in verbose  mode didn't trigger. Therefore, switch to this dataset
     // whenever it's fast enough to be enabled in tests, or somehow create a test facts program
     // or reduce it from clap.
-    let opt = Output::compute(&all_facts, Algorithm::DatafrogOpt, true);
+    let opt = Output::compute(&all_facts, Algorithm::DatafrogOpt(Engine::Datafrog), true);
     assert!(!subset_symmetries_exist(&opt));
     Ok(())
 }
@@ -323,8 +323,8 @@ fn smoke_test_errors() {
         let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts");
 
         let location_insensitive = Output::compute(&facts, Algorithm::LocationInsensitive, true);
-        let naive = Output::compute(&facts, Algorithm::Naive, true);
-        let opt = Output::compute(&facts, Algorithm::DatafrogOpt, true);
+        let naive = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true);
+        let opt = Output::compute(&facts, Algorithm::DatafrogOpt(Engine::Datafrog), true);
 
         // We have to find errors with every analysis
         assert!(
@@ -399,7 +399,7 @@ fn var_live_in_single_block() {
     let mut tables = intern::InternerTables::new();
     let facts = parse_from_program(program, &mut tables).expect("Parsing failure");
 
-    let liveness = Output::compute(&facts, Algorithm::Naive, true).var_live_on_entry;
+    let liveness = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true).var_live_on_entry;
     println!("Registered liveness data: {:?}", liveness);
     for (point, variables) in liveness.iter() {
         println!("{:?} has live variables: {:?}", point, variables);
@@ -433,7 +433,7 @@ fn var_live_in_successor_propagates_to_predecessor() {
     let mut tables = intern::InternerTables::new();
     let facts = parse_from_program(program, &mut tables).expect("Parsing failure");
 
-    let liveness = Output::compute(&facts, Algorithm::Naive, true).var_live_on_entry;
+    let liveness = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true).var_live_on_entry;
     println!("Registered liveness data: {:?}", liveness);
     println!("CFG: {:?}", facts.cfg_edge);
     for (point, variables) in liveness.iter() {
@@ -470,7 +470,7 @@ fn var_live_in_successor_killed_by_reassignment() {
     let mut tables = intern::InternerTables::new();
     let facts = parse_from_program(program, &mut tables).expect("Parsing failure");
 
-    let result = Output::compute(&facts, Algorithm::Naive, true);
+    let result = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true);
     println!("result: {:#?}", result);
     let liveness = result.var_live_on_entry;
     println!("CFG: {:#?}", facts.cfg_edge);
@@ -531,7 +531,7 @@ fn var_drop_used_simple() {
     let mut tables = intern::InternerTables::new();
     let facts = parse_from_program(program, &mut tables).expect("Parsing failure");
 
-    let result = Output::compute(&facts, Algorithm::Naive, true);
+    let result = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true);
     println!("result: {:#?}", result);
     let liveness = result.var_drop_live_on_entry;
     println!("CFG: {:#?}", facts.cfg_edge);
@@ -573,7 +573,7 @@ fn var_drop_used_simple() {
 fn illegal_subset_error() {
     let program = r"
         placeholders { 'a, 'b }
-        
+
         block B0 {
             // creates a transitive `'b: 'a` subset
             loan_issued_at('x, L0),
@@ -638,7 +638,7 @@ fn transitive_known_subset() {
     let program = r"
         placeholders { 'a, 'b, 'c }
         known_subsets { 'a: 'b, 'b: 'c }
-        
+
         block B0 {
             loan_issued_at('x, L0),
               outlives('a: 'x),
@@ -670,7 +670,7 @@ fn transitive_illegal_subset_error() {
     let program = r"
         placeholders { 'a, 'b, 'c }
         known_subsets { 'a: 'b }
-        
+
         block B0 {
             // this transitive `'a: 'b` subset is already known
             loan_issued_at('x, L0),
@@ -679,7 +679,7 @@ fn transitive_illegal_subset_error() {
 
             // creates unknown transitive subsets:
             // - `'b: 'c`
-            // - and therefore `'a: 'c` 
+            // - and therefore `'a: 'c`
             loan_issued_at('y, L1),
               outlives('b: 'y),
               outlives('y: 'c);
@@ -721,15 +721,15 @@ fn successes_in_subset_relations_dataset() {
         let tables = &mut intern::InternerTables::new();
         let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts");
 
-        let naive = Output::compute(&facts, Algorithm::Naive, true);
+        let naive = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true);
         assert!(naive.errors.is_empty());
         assert!(naive.subset_errors.is_empty());
 
         let insensitive = Output::compute(&facts, Algorithm::LocationInsensitive, true);
         assert!(insensitive.errors.is_empty());
         assert!(insensitive.subset_errors.is_empty());
 
-        let opt = Output::compute(&facts, Algorithm::DatafrogOpt, true);
+        let opt = Output::compute(&facts, Algorithm::DatafrogOpt(Engine::Datafrog), true);
         assert!(opt.errors.is_empty());
         assert!(opt.subset_errors.is_empty());
     }
@@ -746,7 +746,7 @@ fn errors_in_subset_relations_dataset() {
     let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts");
 
     // this function has no illegal access errors, but one subset error, over 3 points
-    let naive = Output::compute(&facts, Algorithm::Naive, true);
+    let naive = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true);
     assert!(naive.errors.is_empty());
     assert_eq!(naive.subset_errors.len(), 3);
 
@@ -782,7 +782,7 @@ fn errors_in_subset_relations_dataset() {
     assert!(insensitive_subset_errors.contains(&expected_subset_error));
 
     // And the optimized analysis results should be the same as the naive one's.
-    let opt = Output::compute(&facts, Algorithm::Naive, true);
+    let opt = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true);
     assert_outputs_match(&naive, &opt);
 }
 
@@ -802,7 +802,7 @@ fn successes_in_move_errors_dataset() {
         let tables = &mut intern::InternerTables::new();
         let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts");
 
-        let naive = Output::compute(&facts, Algorithm::Naive, true);
+        let naive = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true);
         assert!(naive.errors.is_empty());
         assert!(naive.subset_errors.is_empty());
         assert!(naive.move_errors.is_empty());
@@ -812,7 +812,7 @@ fn successes_in_move_errors_dataset() {
         assert!(insensitive.subset_errors.is_empty());
         assert!(insensitive.move_errors.is_empty());
 
-        let opt = Output::compute(&facts, Algorithm::DatafrogOpt, true);
+        let opt = Output::compute(&facts, Algorithm::DatafrogOpt(Engine::Datafrog), true);
         assert!(opt.errors.is_empty());
         assert!(opt.subset_errors.is_empty());
         assert!(opt.move_errors.is_empty());
@@ -829,7 +829,7 @@ fn basic_move_error() {
     let tables = &mut intern::InternerTables::new();
     let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts");
 
-    let result = Output::compute(&facts, Algorithm::Naive, true);
+    let result = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true);
     assert!(result.errors.is_empty());
     assert!(result.subset_errors.is_empty());
 
@@ -853,7 +853,7 @@ fn conditional_init() {
     let tables = &mut intern::InternerTables::new();
     let facts = tab_delim::load_tab_delimited_facts(tables, &facts_dir).expect("facts");
 
-    let result = Output::compute(&facts, Algorithm::Naive, true);
+    let result = Output::compute(&facts, Algorithm::Naive(Engine::Datafrog), true);
     assert!(result.errors.is_empty());
     assert!(result.subset_errors.is_empty());
 

src/test_util.rs

@@ -1,6 +1,6 @@
 #![cfg(test)]
 
-use polonius_engine::{Algorithm, AllFacts, Output};
+use polonius_engine::{Algorithm, AllFacts, Engine, Output};
 use std::fmt::Debug;
 
 use crate::facts::LocalFacts;
@@ -76,15 +76,15 @@ pub(crate) fn check_program(
 }
 
 pub(crate) fn naive_checker_for(program: &str) -> FactChecker {
-    check_program(program, Algorithm::Naive, true)
+    check_program(program, Algorithm::Naive(Engine::Datafrog), true)
 }
 
 pub(crate) fn location_insensitive_checker_for(program: &str) -> FactChecker {
     check_program(program, Algorithm::LocationInsensitive, true)
 }
 
 pub(crate) fn opt_checker_for(program: &str) -> FactChecker {
-    check_program(program, Algorithm::DatafrogOpt, true)
+    check_program(program, Algorithm::DatafrogOpt(Engine::Datafrog), true)
 }
 
 pub(crate) fn assert_checkers_match(checker_a: &FactChecker, checker_b: &FactChecker) {