Merge pull request #8 from herbie-fp/unsound

Avoid unsoundness

Author: pavpanchekha

Cargo.toml

@@ -6,7 +6,8 @@ edition = "2018"
 
 
 [dependencies]
-egg = "0.5"
+egg = "0.6"
+
 log = "0.4"
 indexmap = "1"
 libc = "0.2.71"

src/lib.rs

@@ -1,11 +1,12 @@
 pub mod math;
 pub mod rules;
 
+use egg::Id;
 use math::*;
 
 use std::ffi::{CStr, CString};
 use std::os::raw::c_char;
-use std::slice;
+use std::{slice, sync::atomic::Ordering};
 
 unsafe fn cstring_to_recexpr(c_string: *const c_char) -> Option<RecExpr> {
     match CStr::from_ptr(c_string).to_str() {
@@ -79,6 +80,7 @@ pub unsafe extern "C" fn egraph_add_expr(
     expr: *const c_char,
 ) -> *mut EGraphAddResult {
     ffirun(|| {
+        let _ = env_logger::try_init();
         let ctx = &mut *ptr;
         let mut runner = ctx
             .runner
@@ -95,6 +97,7 @@ pub unsafe extern "C" fn egraph_add_expr(
             Some(rec_expr) => {
                 runner = runner.with_expr(&rec_expr);
                 let id = *runner.roots.last().unwrap();
+                let id = usize::from(id) as u32;
                 EGraphAddResult { id, successp: true }
             }
         };
@@ -151,24 +154,38 @@ pub unsafe extern "C" fn egraph_run_iter(
             let rules: Vec<Rewrite> = rules::mk_rules(&ffi_tuples);
 
             runner.egraph.analysis.constant_fold = is_constant_folding_enabled;
-            runner = runner.with_node_limit(limit as usize).run(&rules);
+            runner = runner
+                .with_node_limit(limit as usize)
+                .with_hook(|r| {
+                    if r.egraph.analysis.unsound.load(Ordering::SeqCst) {
+                        Err("Unsoundness detected".into())
+                    } else {
+                        Ok(())
+                    }
+                })
+                .run(&rules);
         }
         ctx.runner = Some(runner);
     })
 }
 
 fn find_extracted(runner: &Runner, id: u32) -> &Extracted {
-    let id = runner.egraph.find(id);
-    let iter = runner
-        .iterations
-        .last()
-        .expect("There should be some iterations by now!");
-    iter.data
+    let id = runner.egraph.find(Id::from(id as usize));
+    let desired_iter = if runner.egraph.analysis.unsound.load(Ordering::SeqCst) {
+        // go back one more iter, add egg can duplicate the final iter in the case of an error
+        runner.iterations.len().saturating_sub(3)
+    } else {
+        runner.iterations.len().saturating_sub(1)
+    };
+
+    runner.iterations[desired_iter]
+        .data
         .extracted
         .iter()
         .find(|(i, _)| runner.egraph.find(*i) == id)
         .map(|(_, ext)| ext)
         .expect("Couldn't find matching extraction!")
+        .clone()
 }
 
 #[no_mangle]

src/math.rs

@@ -1,5 +1,7 @@
 use egg::*;
 
+use std::sync::atomic::{AtomicBool, Ordering};
+
 use num_bigint::BigInt;
 use num_rational::Ratio;
 use num_traits::{Pow, Signed, Zero};
@@ -144,6 +146,7 @@ define_language! {
 }
 
 pub struct ConstantFold {
+    pub unsound: AtomicBool,
     pub constant_fold: bool,
     pub prune: bool,
 }
@@ -153,6 +156,7 @@ impl Default for ConstantFold {
         Self {
             constant_fold: true,
             prune: true,
+            unsound: AtomicBool::from(false),
         }
     }
 }
@@ -210,11 +214,21 @@ impl Analysis<Math> for ConstantFold {
     }
 
     fn merge(&self, to: &mut Self::Data, from: Self::Data) -> bool {
-        if to.is_none() && from.is_some() {
-            *to = from;
-            true
-        } else {
-            false
+        match (&to, from) {
+            (None, None) => false,
+            (Some(_), None) => false, // no update needed
+            (None, Some(c)) => {
+                *to = Some(c);
+                true
+            }
+            (Some(a), Some(ref b)) => {
+                if a != b {
+                    if !self.unsound.swap(true, Ordering::SeqCst) {
+                        log::warn!("Bad merge detected: {} != {}", a, b);
+                    }
+                }
+                false
+            }
         }
     }