Returns a domain that is simplified (refined) by using the current path conditions (conditions known to be true in the current context). If no refinement is possible the result is simply a clone of this domain. This function is performance critical and involves a tricky trade-off: Invoking it is expensive, particularly when expressions get large (hence k_limits::MAX_EXPRESSION_SIZE). One reason f
(&self, path_condition: &Self, depth: usize)
| 1357 | /// the cost of refine_parameters, which is essential. Likewise, it wil also increase the cost |
| 1358 | /// of refine_paths, which ensures that paths stay unique (dealing with aliasing is expensive). |
| 1359 | fn refine_with(&self, path_condition: &Self, depth: usize) -> Rc<SymbolicValue> { |
| 1360 | //do not use false path conditions to refine things |
| 1361 | if depth >= k_limits::MAX_REFINE_DEPTH { |
| 1362 | //todo: perhaps this should go away. |
| 1363 | // right now it deals with the situation where some large expressions have sizes |
| 1364 | // that are not accurately tracked. These really should get fixed. |
| 1365 | return self.clone(); |
| 1366 | } |
| 1367 | // In this context path_condition is true |
| 1368 | if path_condition.eq(self) { |
| 1369 | return Rc::new(SymbolicValue::new_true()); |
| 1370 | } |
| 1371 | |
| 1372 | // If the path context constrains the self expression to be equal to a constant, just |
| 1373 | // return the constant. |
| 1374 | if let Expression::Equals { left, right } = &path_condition.expression { |
| 1375 | if let Expression::CompileTimeConstant(..) = &left.expression { |
| 1376 | if self.eq(right) { |
| 1377 | return left.clone(); |
| 1378 | } |
| 1379 | } |
| 1380 | if let Expression::CompileTimeConstant(..) = &right.expression { |
| 1381 | if self.eq(left) { |
| 1382 | return right.clone(); |
| 1383 | } |
| 1384 | } |
| 1385 | } |
| 1386 | // Traverse the self expression, looking for recursive refinement opportunities. |
| 1387 | // Important, keep the traversal as trivial as possible and put optimizations in |
| 1388 | // the transfer functions. Also, keep the transfer functions constant in cost as |
| 1389 | // much as possible. Any time they are not, this function becomes quadratic and |
| 1390 | // performance becomes terrible. |
| 1391 | match &self.expression { |
| 1392 | Expression::Drop(..) => self.clone(), |
| 1393 | Expression::Numerical(..) => self.clone(), |
| 1394 | Expression::Bottom | Expression::Top => self.clone(), |
| 1395 | Expression::And { left, right } => left |
| 1396 | .refine_with(path_condition, depth + 1) |
| 1397 | .and(right.refine_with(path_condition, depth + 1)), |
| 1398 | Expression::Cast { |
| 1399 | operand, |
| 1400 | target_type, |
| 1401 | } => operand |
| 1402 | .refine_with(path_condition, depth + 1) |
| 1403 | .cast(target_type.clone()), |
| 1404 | Expression::CompileTimeConstant(..) => self.clone(), |
| 1405 | Expression::Equals { left, right } => left |
| 1406 | .refine_with(path_condition, depth + 1) |
| 1407 | .equals(right.refine_with(path_condition, depth + 1)), |
| 1408 | Expression::GreaterOrEqual { left, right } => left |
| 1409 | .refine_with(path_condition, depth + 1) |
| 1410 | .greater_or_equal(right.refine_with(path_condition, depth + 1)), |
| 1411 | Expression::GreaterThan { left, right } => left |
| 1412 | .refine_with(path_condition, depth + 1) |
| 1413 | .greater_than(right.refine_with(path_condition, depth + 1)), |
| 1414 | Expression::HeapBlock { .. } => self.clone(), |
| 1415 | Expression::Join { left, right } => left |
| 1416 | .refine_with(path_condition, depth + 1) |
no test coverage detected