Merge pull request #75 from DiuDiu777/senryx

Fix contracts checking bugs in senryx
Artisan-Lab · Nov 16, 2024 · a32584e · a32584e
2 parents 0c0057f + 13236de
commit a32584e
Show file tree

Hide file tree

Showing 9 changed files with 321 additions and 148 deletions.
diff --git a/rap/src/analysis/senryx.rs b/rap/src/analysis/senryx.rs
@@ -58,11 +58,11 @@ impl<'tcx> SenryxCheck<'tcx> {
     pub fn pre_handle_type(&self, def_id: DefId) {
         let mut uig_checker = UnsafetyIsolationCheck::new(self.tcx);
         let func_type = uig_checker.get_type(def_id);
-        let mut body_visitor = BodyVisitor::new(self.tcx, def_id, true);
+        let mut body_visitor = BodyVisitor::new(self.tcx, def_id, 0);
         if func_type == 1 {
             let func_cons = uig_checker.search_constructor(def_id);
             for func_con in func_cons {
-                let mut cons_body_visitor = BodyVisitor::new(self.tcx, func_con, true);
+                let mut cons_body_visitor = BodyVisitor::new(self.tcx, func_con, 0);
                 cons_body_visitor.path_forward_check();
                 // TODO: cache fields' states
 

diff --git a/rap/src/analysis/senryx/contracts/abstract_state.rs b/rap/src/analysis/senryx/contracts/abstract_state.rs
@@ -45,8 +45,9 @@ pub enum AllocatedState {
 #[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)]
 pub enum AlignState {
     Aligned,
-    Small2BigCast,
-    Big2SmallCast,
+    Small2BigCast(usize, usize),
+    Big2SmallCast(usize, usize),
+    Unaligned,
 }
 
 #[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)]
@@ -109,7 +110,7 @@ impl AbstractStateItem {
 
 #[derive(PartialEq)]
 pub struct AbstractState {
-    pub state_map: HashMap<usize, AbstractStateItem>,
+    pub state_map: HashMap<usize, Option<AbstractStateItem>>,
 }
 
 impl AbstractState {
@@ -119,7 +120,7 @@ impl AbstractState {
         }
     }
 
-    pub fn insert_abstate(&mut self, place: usize, place_state_item: AbstractStateItem) {
+    pub fn insert_abstate(&mut self, place: usize, place_state_item: Option<AbstractStateItem>) {
         self.state_map.insert(place, place_state_item);
     }
 }
diff --git a/rap/src/analysis/senryx/contracts/checker.rs b/rap/src/analysis/senryx/contracts/checker.rs
@@ -30,8 +30,8 @@ impl<T> SliceFromRawPartsChecker<T> {
                     state: StateType::AllocatedState(AllocatedState::Alloc),
                 },
                 Contract::StateCheck {
-                    op: Op::NE,
-                    state: StateType::AlignState(AlignState::Small2BigCast),
+                    op: Op::GT,
+                    state: StateType::AlignState(AlignState::Unaligned),
                 },
             ],
         );

diff --git a/rap/src/analysis/senryx/contracts/contract.rs b/rap/src/analysis/senryx/contracts/contract.rs
@@ -14,7 +14,9 @@ pub fn check_contract(contract: Contract, abstate_item: &AbstractStateItem) -> b
         }
         Contract::StateCheck { op, state } => {
             for ab_state in &abstate_item.state {
-                if handle_state_op(*ab_state, op, state) {
+                if check_is_same_state_type(ab_state, &state)
+                    && handle_state_op(*ab_state, op, state)
+                {
                     return true;
                 }
             }
@@ -23,6 +25,18 @@ pub fn check_contract(contract: Contract, abstate_item: &AbstractStateItem) -> b
     }
 }
 
+pub fn check_is_same_state_type(left: &StateType, right: &StateType) -> bool {
+    match (*left, *right) {
+        (StateType::AllocatedState(_), StateType::AllocatedState(_)) => {
+            return true;
+        }
+        (StateType::AlignState(_), StateType::AlignState(_)) => {
+            return true;
+        }
+        _ => false,
+    }
+}
+
 pub fn handle_value_op<T: std::cmp::PartialEq + std::cmp::PartialOrd>(
     left: &(T, T),
     op: Op,

diff --git a/rap/src/analysis/senryx/contracts/state_lattice.rs b/rap/src/analysis/senryx/contracts/state_lattice.rs
@@ -131,27 +131,35 @@ impl Lattice for AlignState {
     fn join(&self, other: Self) -> Self {
         match (self, other) {
             (AlignState::Aligned, _) => AlignState::Aligned,
-            (AlignState::Big2SmallCast, AlignState::Big2SmallCast) => AlignState::Big2SmallCast,
-            (AlignState::Big2SmallCast, AlignState::Small2BigCast) => AlignState::Big2SmallCast,
-            (AlignState::Big2SmallCast, AlignState::Aligned) => AlignState::Aligned,
-            (AlignState::Small2BigCast, _) => other,
+            (AlignState::Big2SmallCast(_, _), AlignState::Big2SmallCast(_, _)) => {
+                AlignState::Aligned
+            }
+            (AlignState::Big2SmallCast(_, _), AlignState::Small2BigCast(_, _)) => {
+                AlignState::Unaligned
+            }
+            (AlignState::Big2SmallCast(_, _), AlignState::Aligned) => AlignState::Aligned,
+            (AlignState::Unaligned, _) => AlignState::Unaligned,
+            (_, AlignState::Unaligned) => AlignState::Unaligned,
+            _ => other,
         }
     }
 
     fn meet(&self, other: Self) -> Self {
-        match (self, other) {
-            (AlignState::Aligned, _) => other,
-            (AlignState::Big2SmallCast, AlignState::Big2SmallCast) => AlignState::Big2SmallCast,
-            (AlignState::Big2SmallCast, AlignState::Small2BigCast) => AlignState::Small2BigCast,
-            (AlignState::Big2SmallCast, AlignState::Aligned) => AlignState::Big2SmallCast,
-            (AlignState::Small2BigCast, _) => AlignState::Small2BigCast,
-        }
+        other
+        // match (self, other) {
+        //     (AlignState::Aligned, _) => other,
+        //     (AlignState::Big2SmallCast(_,_), AlignState::Big2SmallCast(_,_)) => AlignState::Aligned,
+        //     (AlignState::Big2SmallCast(_,_), AlignState::Small2BigCast(_,_)) => AlignState::Unaligned,
+        //     (AlignState::Big2SmallCast(_,_), AlignState::Aligned) => AlignState::Big2SmallCast(_,_),
+        //     (AlignState::Small2BigCast, _) => AlignState::Small2BigCast,
+        // }
     }
 
     fn less_than(&self, other: Self) -> bool {
         match (self, other) {
             (_, AlignState::Aligned) => true,
-            (AlignState::Small2BigCast, AlignState::Big2SmallCast) => true,
+            (AlignState::Small2BigCast(_, _), AlignState::Big2SmallCast(_, _)) => true,
+            (AlignState::Small2BigCast(_, _), AlignState::Unaligned) => true,
             _ => false,
         }
     }

diff --git a/rap/src/analysis/senryx/inter_record.rs b/rap/src/analysis/senryx/inter_record.rs
@@ -11,22 +11,25 @@ lazy_static! {
 // static mut GLOBAL_INTER_RECORDER: HashMap<DefId,InterAnalysisRecord> = HashMap::new();
 
 pub struct InterAnalysisRecord {
-    pub pre_analysis_state: HashMap<usize, AbstractStateItem>,
-    pub post_analysis_state: HashMap<usize, AbstractStateItem>,
+    pub pre_analysis_state: HashMap<usize, Option<AbstractStateItem>>,
+    pub post_analysis_state: HashMap<usize, Option<AbstractStateItem>>,
 }
 
 impl InterAnalysisRecord {
     pub fn new(
-        pre_analysis_state: HashMap<usize, AbstractStateItem>,
-        post_analysis_state: HashMap<usize, AbstractStateItem>,
+        pre_analysis_state: HashMap<usize, Option<AbstractStateItem>>,
+        post_analysis_state: HashMap<usize, Option<AbstractStateItem>>,
     ) -> Self {
         Self {
             pre_analysis_state,
             post_analysis_state,
         }
     }
 
-    pub fn is_pre_state_same(&self, other_pre_state: &HashMap<usize, AbstractStateItem>) -> bool {
+    pub fn is_pre_state_same(
+        &self,
+        other_pre_state: &HashMap<usize, Option<AbstractStateItem>>,
+    ) -> bool {
         self.pre_analysis_state == *other_pre_state
     }
 }
diff --git a/rap/src/analysis/senryx/matcher.rs b/rap/src/analysis/senryx/matcher.rs
@@ -32,10 +32,10 @@ fn process_checker(checker: &dyn Checker, args: &Box<[Spanned<Operand>]>, abstat
         for contract in contracts_vec {
             let arg_place = get_arg_place(&args[*idx].node);
             if arg_place == 0 {
-                return;
+                continue;
             }
             if let Some(abstate_item) = abstate.state_map.get(&arg_place) {
-                if !check_contract(*contract, abstate_item) {
+                if !check_contract(*contract, &abstate_item.clone().unwrap()) {
                     println!("Contract failed! ---- {:?}", contract);
                 } else {
                     println!("Contract passed! ---- {:?}", contract);