oxilean_kernel/abstract_interp/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::types::{
6    AbstractAlarm, AbstractCmp, AbstractInterpreter, AbstractState, AbstractTrace, AlarmCollector,
7    AlarmSeverity, AnalysisConfig, AnalysisResults, BlockReachability, CallGraph, CallGraphNode,
8    ChaoticIterator, CongruenceDomain, CostBound, DepthDomain, FixpointEngine, FunctionSummary,
9    InterpretationSummary, Interval, IntervalEnv, IntervalParityProduct, NullnessDomain,
10    ParityDomain, PowersetDomain, ReachabilityAnalysis, SignDomain, SimpleAbstractInterpreter,
11    SizeDomain, SummaryDatabase, TerminationEvidence, TransferEffect, TransferFunction,
12    TrileanDomain,
13};
14
15/// A lattice-based abstract domain for static analysis.
16pub trait AbstractDomain: Sized {
17    /// Least upper bound (join) of two elements.
18    fn join(&self, other: &Self) -> Self;
19    /// Greatest lower bound (meet) of two elements.
20    fn meet(&self, other: &Self) -> Self;
21    /// True if this element is bottom (least element).
22    fn is_bottom(&self) -> bool;
23    /// True if this element is top (greatest element).
24    fn is_top(&self) -> bool;
25    /// True if `self ⊑ other`.
26    fn leq(&self, other: &Self) -> bool;
27}
28#[cfg(test)]
29mod tests {
30    use super::*;
31    #[test]
32    fn test_sign_domain_join() {
33        assert_eq!(SignDomain::Pos.join(&SignDomain::Zero), SignDomain::NonNeg);
34        assert_eq!(SignDomain::Neg.join(&SignDomain::Pos), SignDomain::Nonzero);
35        assert_eq!(SignDomain::Bottom.join(&SignDomain::Pos), SignDomain::Pos);
36        assert_eq!(SignDomain::Top.join(&SignDomain::Neg), SignDomain::Top);
37    }
38    #[test]
39    fn test_sign_domain_leq() {
40        assert!(SignDomain::Bottom.leq(&SignDomain::Pos));
41        assert!(SignDomain::Pos.leq(&SignDomain::NonNeg));
42        assert!(SignDomain::NonNeg.leq(&SignDomain::Top));
43        assert!(!SignDomain::Pos.leq(&SignDomain::Neg));
44    }
45    #[test]
46    fn test_sign_negate() {
47        assert_eq!(SignDomain::Pos.negate(), SignDomain::Neg);
48        assert_eq!(SignDomain::Neg.negate(), SignDomain::Pos);
49        assert_eq!(SignDomain::Zero.negate(), SignDomain::Zero);
50        assert_eq!(SignDomain::NonNeg.negate(), SignDomain::NonPos);
51        assert_eq!(SignDomain::Top.negate(), SignDomain::Top);
52        assert_eq!(SignDomain::Bottom.negate(), SignDomain::Bottom);
53    }
54    #[test]
55    fn test_depth_domain_increase() {
56        let d = DepthDomain::new(10);
57        assert_eq!(d.current_depth, 0);
58        let d2 = d.increase();
59        assert_eq!(d2.current_depth, 1);
60        assert!(d2.is_bounded());
61    }
62    #[test]
63    fn test_size_domain_add() {
64        let a = SizeDomain::Small(3);
65        let b = SizeDomain::Small(4);
66        assert_eq!(SizeDomain::add(a, b), SizeDomain::Small(7));
67        let c = SizeDomain::Zero;
68        assert_eq!(
69            SizeDomain::add(c, SizeDomain::Small(5)),
70            SizeDomain::Small(5)
71        );
72        assert_eq!(
73            SizeDomain::add(SizeDomain::Bottom, SizeDomain::Large),
74            SizeDomain::Bottom
75        );
76    }
77    #[test]
78    fn test_abstract_state_join() {
79        let s1 = AbstractState {
80            sign: SignDomain::Pos,
81            depth: DepthDomain::new(10),
82            size: SizeDomain::Small(5),
83        };
84        let s2 = AbstractState {
85            sign: SignDomain::Neg,
86            depth: DepthDomain {
87                max_depth: 10,
88                current_depth: 3,
89            },
90            size: SizeDomain::Small(8),
91        };
92        let joined = s1.join(&s2);
93        assert_eq!(joined.sign, SignDomain::Nonzero);
94        assert_eq!(joined.depth.current_depth, 3);
95        assert_eq!(joined.size, SizeDomain::Small(8));
96    }
97    #[test]
98    fn test_interpreter_analyze_depth() {
99        let interp = AbstractInterpreter::new(100);
100        let d = interp.analyze_depth("((a b) (c (d e)))");
101        assert_eq!(d.current_depth, 3);
102        assert!(d.is_bounded());
103    }
104    #[test]
105    fn test_fixed_point_convergence() {
106        let interp = AbstractInterpreter::new(100);
107        let result = interp.fixed_point(42u64, |x| *x);
108        assert_eq!(result, 42);
109        let result2 = interp.fixed_point(0u64, |x| (*x + 1).min(10));
110        assert_eq!(result2, 10);
111    }
112}
113/// Widening operator for interval environments.
114#[allow(dead_code)]
115pub fn widen_env(old: &IntervalEnv, new: &IntervalEnv) -> IntervalEnv {
116    let mut result = IntervalEnv::new();
117    for (name, old_iv) in &old.bindings {
118        let new_iv = new.get(name);
119        let lo = if new_iv.lo < old_iv.lo {
120            i64::MIN
121        } else {
122            old_iv.lo
123        };
124        let hi = if new_iv.hi > old_iv.hi {
125            i64::MAX
126        } else {
127            old_iv.hi
128        };
129        result.set(name, Interval { lo, hi });
130    }
131    result
132}
133/// Narrowing operator for interval environments.
134#[allow(dead_code)]
135pub fn narrow_env(wide: &IntervalEnv, precise: &IntervalEnv) -> IntervalEnv {
136    let mut result = IntervalEnv::new();
137    for (name, wide_iv) in &wide.bindings {
138        let prec_iv = precise.get(name);
139        let lo = if wide_iv.lo == i64::MIN {
140            prec_iv.lo
141        } else {
142            wide_iv.lo
143        };
144        let hi = if wide_iv.hi == i64::MAX {
145            prec_iv.hi
146        } else {
147            wide_iv.hi
148        };
149        result.set(name, Interval { lo, hi });
150    }
151    result
152}
153#[cfg(test)]
154mod tests_abstract_extended {
155    use super::*;
156    #[test]
157    fn test_interval_basics() {
158        let iv = Interval::new(3, 7);
159        assert!(iv.contains(5));
160        assert!(!iv.contains(2));
161        assert_eq!(iv.width(), 5);
162        let bottom = Interval::bottom();
163        assert!(bottom.is_bottom());
164        let top = Interval::top();
165        assert!(top.is_top());
166    }
167    #[test]
168    fn test_interval_join_meet() {
169        let a = Interval::new(1, 5);
170        let b = Interval::new(3, 10);
171        let joined = a.join(&b);
172        assert_eq!(joined.lo, 1);
173        assert_eq!(joined.hi, 10);
174        let met = a.meet(&b);
175        assert_eq!(met.lo, 3);
176        assert_eq!(met.hi, 5);
177    }
178    #[test]
179    fn test_interval_arithmetic() {
180        let a = Interval::new(1, 5);
181        let b = Interval::new(2, 3);
182        let sum = a.add(&b);
183        assert_eq!(sum.lo, 3);
184        assert_eq!(sum.hi, 8);
185        let diff = a.sub(&b);
186        assert_eq!(diff.lo, -2);
187        assert_eq!(diff.hi, 3);
188    }
189    #[test]
190    fn test_parity_domain_join() {
191        use ParityDomain::*;
192        assert_eq!(Even.join(&Even), Even);
193        assert_eq!(Even.join(&Odd), Top);
194        assert_eq!(Bottom.join(&Odd), Odd);
195    }
196    #[test]
197    fn test_parity_domain_arithmetic() {
198        use ParityDomain::*;
199        assert_eq!(Even.add(&Odd), Odd);
200        assert_eq!(Odd.add(&Odd), Even);
201        assert_eq!(Even.mul(&Odd), Even);
202        assert_eq!(Odd.mul(&Odd), Odd);
203    }
204    #[test]
205    fn test_nullness_domain() {
206        use NullnessDomain::*;
207        assert!(Null.may_be_null());
208        assert!(Top.may_be_null());
209        assert!(!NonNull.may_be_null());
210        assert_eq!(Null.join(&NonNull), Top);
211        assert!(NonNull.is_definitely_non_null());
212    }
213    #[test]
214    fn test_interval_env() {
215        let mut env = IntervalEnv::new();
216        env.set("x", Interval::new(0, 10));
217        env.set("y", Interval::new(5, 15));
218        let x = env.get("x");
219        assert_eq!(x.lo, 0);
220        assert_eq!(x.hi, 10);
221        let mut env2 = IntervalEnv::new();
222        env2.set("x", Interval::new(3, 20));
223        env2.set("z", Interval::new(1, 1));
224        let joined = env.join(&env2);
225        let xj = joined.get("x");
226        assert_eq!(xj.lo, 0);
227        assert_eq!(xj.hi, 20);
228    }
229    #[test]
230    fn test_fixpoint_engine() {
231        let mut engine = FixpointEngine::new(10);
232        assert!(!engine.is_exhausted());
233        for _ in 0..10 {
234            engine.step();
235        }
236        assert!(engine.is_exhausted());
237        engine.reset();
238        assert_eq!(engine.iterations(), 0);
239    }
240    #[test]
241    fn test_fixpoint_detection() {
242        let mut env1 = IntervalEnv::new();
243        env1.set("x", Interval::new(0, 10));
244        let mut env2 = IntervalEnv::new();
245        env2.set("x", Interval::new(0, 10));
246        assert!(FixpointEngine::is_fixpoint(&env1, &env2));
247        env2.set("x", Interval::new(0, 11));
248        assert!(!FixpointEngine::is_fixpoint(&env1, &env2));
249    }
250    #[test]
251    fn test_widen_env() {
252        let mut old = IntervalEnv::new();
253        old.set("x", Interval::new(0, 5));
254        let mut new = IntervalEnv::new();
255        new.set("x", Interval::new(0, 10));
256        let widened = widen_env(&old, &new);
257        let xw = widened.get("x");
258        assert_eq!(xw.lo, 0);
259        assert_eq!(xw.hi, i64::MAX);
260    }
261    #[test]
262    fn test_narrow_env() {
263        let mut wide = IntervalEnv::new();
264        wide.set(
265            "x",
266            Interval {
267                lo: i64::MIN,
268                hi: i64::MAX,
269            },
270        );
271        let mut precise = IntervalEnv::new();
272        precise.set("x", Interval::new(-100, 100));
273        let narrowed = narrow_env(&wide, &precise);
274        let xn = narrowed.get("x");
275        assert_eq!(xn.lo, -100);
276        assert_eq!(xn.hi, 100);
277    }
278}
279#[cfg(test)]
280mod tests_abstract_extended2 {
281    use super::*;
282    #[test]
283    fn test_congruence_domain_satisfies() {
284        let even = CongruenceDomain::congruent(2, 0);
285        assert!(even.satisfies(4));
286        assert!(!even.satisfies(3));
287        let top = CongruenceDomain::top();
288        assert!(top.satisfies(999));
289        let bottom = CongruenceDomain::bottom();
290        assert!(!bottom.satisfies(0));
291    }
292    #[test]
293    fn test_congruence_domain_join() {
294        let a = CongruenceDomain::congruent(4, 0);
295        let b = CongruenceDomain::congruent(4, 0);
296        let joined = a.join(&b);
297        assert!(!joined.is_top());
298        let c = CongruenceDomain::congruent(4, 1);
299        let joined2 = a.join(&c);
300        assert!(joined2.is_top());
301    }
302    #[test]
303    fn test_powerset_domain() {
304        let mut s = PowersetDomain::bottom(8);
305        assert!(s.is_bottom());
306        s.add(0);
307        s.add(3);
308        s.add(7);
309        assert_eq!(s.count(), 3);
310        assert!(s.contains(3));
311        assert!(!s.contains(2));
312        s.remove(3);
313        assert!(!s.contains(3));
314        let t = PowersetDomain::top(8);
315        assert!(t.is_top());
316        assert_eq!(t.count(), 8);
317    }
318    #[test]
319    fn test_powerset_join_meet() {
320        let mut a = PowersetDomain::bottom(4);
321        a.add(0);
322        a.add(1);
323        let mut b = PowersetDomain::bottom(4);
324        b.add(1);
325        b.add(2);
326        let joined = a.join(&b);
327        assert!(joined.contains(0) && joined.contains(1) && joined.contains(2));
328        let met = a.meet(&b);
329        assert!(met.contains(1));
330        assert!(!met.contains(0));
331        assert!(!met.contains(2));
332    }
333    #[test]
334    fn test_chaotic_iterator() {
335        let mut iter = ChaoticIterator::new(5);
336        for _ in 0..3 {
337            assert!(iter.advance());
338        }
339        iter.mark_converged();
340        assert!(iter.is_converged());
341        assert!(!iter.is_limit_exceeded());
342        assert_eq!(iter.steps(), 3);
343    }
344    #[test]
345    fn test_chaotic_iterator_limit() {
346        let mut iter = ChaoticIterator::new(3);
347        for _ in 0..3 {
348            iter.advance();
349        }
350        assert!(!iter.advance());
351        assert!(iter.is_limit_exceeded());
352    }
353    #[test]
354    fn test_abstract_trace() {
355        let mut trace = AbstractTrace::new();
356        trace.record("loop_head", Interval::new(0, 10));
357        trace.record("loop_body", Interval::new(1, 10));
358        assert_eq!(trace.at("loop_head"), Some(Interval::new(0, 10)));
359        assert_eq!(trace.at("exit"), None);
360        let fmt = trace.format();
361        assert!(fmt.contains("loop_head: [0, 10]"));
362    }
363    #[test]
364    fn test_alarm_collector() {
365        let mut ac = AlarmCollector::new();
366        ac.add(AbstractAlarm::new(
367            "L1",
368            "possible null",
369            AlarmSeverity::Warning,
370        ));
371        ac.add(AbstractAlarm::new(
372            "L2",
373            "division by zero",
374            AlarmSeverity::Error,
375        ));
376        ac.add(AbstractAlarm::new("L3", "info msg", AlarmSeverity::Info));
377        assert!(ac.has_errors());
378        assert_eq!(ac.errors().len(), 1);
379        let (info, warn, err) = ac.count_by_severity();
380        assert_eq!((info, warn, err), (1, 1, 1));
381    }
382}
383#[cfg(test)]
384mod tests_abstract_extended3 {
385    use super::*;
386    #[test]
387    fn test_call_graph() {
388        let mut g = CallGraph::new();
389        let mut f = CallGraphNode::new("fact");
390        f.add_callee("fact");
391        f.add_callee("Nat.sub");
392        g.add_node(f);
393        let mut h = CallGraphNode::new("helper");
394        h.add_callee("fact");
395        g.add_node(h);
396        assert!(
397            g.find("fact")
398                .expect("value should be present")
399                .is_recursive
400        );
401        let recursive = g.recursive_fns();
402        assert!(recursive.contains(&"fact"));
403        let callers = g.callers_of("fact");
404        assert!(callers.contains(&"helper"));
405        assert!(callers.contains(&"fact"));
406    }
407    #[test]
408    fn test_reachability_analysis() {
409        let mut ra = ReachabilityAnalysis::new();
410        ra.mark_reachable("entry");
411        ra.mark_reachable("loop");
412        ra.mark_unreachable("dead_code");
413        assert!(ra.is_reachable("entry"));
414        assert!(ra.is_unreachable("dead_code"));
415        assert!(!ra.is_reachable("unknown_label"));
416        assert_eq!(ra.reachable_count(), 2);
417        assert_eq!(ra.unreachable_count(), 1);
418    }
419    #[test]
420    fn test_termination_evidence() {
421        let e1 = TerminationEvidence::Structural { arg_index: 0 };
422        assert!(e1.is_proven());
423        assert!(e1.describe().contains("structural"));
424        let e2 = TerminationEvidence::Lexicographic {
425            measures: vec!["n".to_string(), "m".to_string()],
426        };
427        assert!(e2.describe().contains("lexicographic"));
428        let e3 = TerminationEvidence::Unknown;
429        assert!(!e3.is_proven());
430    }
431    #[test]
432    fn test_cost_bound() {
433        let exact = CostBound::exact(10);
434        assert!(exact.is_bounded());
435        assert_eq!(exact.width(), Some(0));
436        let range = CostBound::range(5, 20);
437        assert_eq!(range.width(), Some(15));
438        let open = CostBound::at_least(3);
439        assert!(!open.is_bounded());
440        let sum = exact.add(&range);
441        assert_eq!(sum.lower, 15);
442        assert_eq!(sum.upper, Some(30));
443        let sum2 = exact.add(&open);
444        assert!(!sum2.is_bounded());
445    }
446}
447#[cfg(test)]
448mod tests_abstract_extended4 {
449    use super::*;
450    #[test]
451    fn test_transfer_function_apply() {
452        let mut env = IntervalEnv::new();
453        env.set("x", Interval::new(0, 10));
454        env.set("y", Interval::new(5, 15));
455        let mut tf = TransferFunction::new("incr_x");
456        tf.add_effect(TransferEffect::Assign {
457            var: "x".to_string(),
458            interval: Interval::new(1, 11),
459        });
460        tf.add_effect(TransferEffect::Invalidate {
461            var: "y".to_string(),
462        });
463        let new_env = tf.apply(&env);
464        let x = new_env.get("x");
465        assert_eq!(x.lo, 1);
466        assert_eq!(x.hi, 11);
467        let y = new_env.get("y");
468        assert!(y.is_top());
469    }
470    #[test]
471    fn test_transfer_function_constrain() {
472        let mut env = IntervalEnv::new();
473        env.set("n", Interval::new(0, 100));
474        let mut tf = TransferFunction::new("guard_n_gt_50");
475        tf.add_effect(TransferEffect::Constrain {
476            var: "n".to_string(),
477            constraint: Interval::new(51, i64::MAX),
478        });
479        let new_env = tf.apply(&env);
480        let n = new_env.get("n");
481        assert_eq!(n.lo, 51);
482        assert_eq!(n.hi, 100);
483    }
484    #[test]
485    fn test_function_summary() {
486        let mut summary = FunctionSummary::new("fact");
487        summary.termination = TerminationEvidence::Structural { arg_index: 0 };
488        summary.cost = CostBound::range(1, 1000);
489        assert!(summary.terminates());
490        let desc = summary.describe();
491        assert!(desc.contains("fact"));
492        assert!(desc.contains("terminates=true"));
493    }
494    #[test]
495    fn test_summary_database() {
496        let mut db = SummaryDatabase::new();
497        let mut s1 = FunctionSummary::new("f");
498        s1.termination = TerminationEvidence::Structural { arg_index: 0 };
499        db.add(s1);
500        let mut s2 = FunctionSummary::new("g");
501        s2.termination = TerminationEvidence::Unknown;
502        db.add(s2);
503        let proven = db.proven_terminating();
504        assert!(proven.contains(&"f"));
505        assert!(!proven.contains(&"g"));
506        assert_eq!(db.len(), 2);
507    }
508}
509#[cfg(test)]
510mod tests_abstract_extended5 {
511    use super::*;
512    #[test]
513    fn test_trilean_and_or_not() {
514        use TrileanDomain::*;
515        assert_eq!(True.and(&False), False);
516        assert_eq!(True.and(&Top), Top);
517        assert_eq!(False.or(&True), True);
518        assert_eq!(False.or(&Top), Top);
519        assert_eq!(True.not(), False);
520        assert_eq!(Top.not(), Top);
521    }
522    #[test]
523    fn test_trilean_join() {
524        use TrileanDomain::*;
525        assert_eq!(True.join(&False), Top);
526        assert_eq!(True.join(&True), True);
527        assert_eq!(False.join(&Bottom), False);
528    }
529    #[test]
530    fn test_block_reachability() {
531        use BlockReachability::*;
532        assert_eq!(Unreachable.join(&Reachable), Reachable);
533        assert_eq!(Unreachable.join(&Unknown), Unknown);
534        assert!(!Unreachable.may_be_reachable());
535        assert!(Unknown.may_be_reachable());
536        assert!(Reachable.may_be_reachable());
537    }
538    #[test]
539    fn test_analysis_config() {
540        let cfg = AnalysisConfig::default_config();
541        assert_eq!(cfg.max_iterations, 100);
542        assert!(cfg.use_widening);
543        assert!(cfg.collect_alarms);
544        let fast = AnalysisConfig::fast();
545        assert_eq!(fast.max_iterations, 10);
546        assert!(!fast.collect_alarms);
547    }
548}
549#[cfg(test)]
550mod tests_abstract_product {
551    use super::*;
552    #[test]
553    fn test_interval_parity_product_basics() {
554        let p = IntervalParityProduct::from_value(4);
555        assert_eq!(p.interval, Interval::new(4, 4));
556        assert_eq!(p.parity, ParityDomain::Even);
557        let p2 = IntervalParityProduct::from_value(7);
558        assert_eq!(p2.parity, ParityDomain::Odd);
559        let joined = p.join(&p2);
560        assert_eq!(joined.interval, Interval::new(4, 7));
561        assert_eq!(joined.parity, ParityDomain::Top);
562    }
563    #[test]
564    fn test_interval_parity_add() {
565        let even = IntervalParityProduct::from_value(4);
566        let odd = IntervalParityProduct::from_value(3);
567        let sum = even.add(&odd);
568        assert_eq!(sum.parity, ParityDomain::Odd);
569        assert_eq!(sum.interval.lo, 7);
570        assert_eq!(sum.interval.hi, 7);
571    }
572    #[test]
573    fn test_analysis_results() {
574        let mut results = AnalysisResults::new();
575        results.set("x", IntervalParityProduct::from_value(4));
576        results.set("y", IntervalParityProduct::from_value(3));
577        results.set(
578            "z",
579            IntervalParityProduct::new(Interval::new(0, 100), ParityDomain::Even),
580        );
581        let non_neg = results.proven_non_negative();
582        assert!(non_neg.contains(&"x") && non_neg.contains(&"y") && non_neg.contains(&"z"));
583        let even_vars = results.proven_even();
584        assert!(even_vars.contains(&"x"));
585        assert!(even_vars.contains(&"z"));
586        assert!(!even_vars.contains(&"y"));
587    }
588}
589#[cfg(test)]
590mod tests_abstract_interp_entry {
591    use super::*;
592    #[test]
593    fn test_interpretation_summary() {
594        let s = InterpretationSummary::new(5, true, 0);
595        assert!(s.proven_safe);
596        assert!(s.describe().contains("safe=true"));
597        let s2 = InterpretationSummary::new(5, true, 3);
598        assert!(!s2.proven_safe);
599    }
600    #[test]
601    fn test_simple_abstract_interpreter() {
602        let cfg = AnalysisConfig::fast();
603        let mut interp = SimpleAbstractInterpreter::new(cfg);
604        interp.init_var("n", IntervalParityProduct::from_value(10));
605        let summary = interp.run_stub();
606        assert!(summary.converged);
607        let r = interp
608            .results()
609            .get("n")
610            .expect("element at \'n\' should exist");
611        assert_eq!(r.interval.lo, 10);
612    }
613}
614#[cfg(test)]
615mod tests_abstract_cmp {
616    use super::*;
617    #[test]
618    fn test_abstract_lt() {
619        let a = Interval::new(1, 5);
620        let b = Interval::new(10, 20);
621        assert_eq!(AbstractCmp::lt(&a, &b), AbstractCmp::DefinitelyTrue);
622        let c = Interval::new(15, 25);
623        assert_eq!(AbstractCmp::lt(&c, &b), AbstractCmp::Unknown);
624        let d = Interval::new(20, 30);
625        assert_eq!(AbstractCmp::lt(&d, &b), AbstractCmp::DefinitelyFalse);
626    }
627    #[test]
628    fn test_abstract_eq() {
629        let a = Interval::new(5, 5);
630        let b = Interval::new(5, 5);
631        assert_eq!(AbstractCmp::eq(&a, &b), AbstractCmp::DefinitelyTrue);
632        let c = Interval::new(1, 3);
633        let d = Interval::new(10, 20);
634        assert_eq!(AbstractCmp::eq(&c, &d), AbstractCmp::DefinitelyFalse);
635        let e = Interval::new(1, 10);
636        assert_eq!(AbstractCmp::eq(&a, &e), AbstractCmp::Unknown);
637    }
638}
639/// Compute the abstract division `a / b` for intervals.
640/// Returns Top (full interval) if `b` contains 0.
641#[allow(dead_code)]
642pub fn abstract_div(a: &Interval, b: &Interval) -> Interval {
643    if a.is_bottom() || b.is_bottom() {
644        return Interval::bottom();
645    }
646    if b.contains(0) {
647        return Interval::top();
648    }
649    let combos = [a.lo / b.lo, a.lo / b.hi, a.hi / b.lo, a.hi / b.hi];
650    let lo = *combos
651        .iter()
652        .min()
653        .expect("combos iterator must be non-empty");
654    let hi = *combos
655        .iter()
656        .max()
657        .expect("combos iterator must be non-empty");
658    Interval::new(lo, hi)
659}
660#[cfg(test)]
661mod tests_abstract_div {
662    use super::*;
663    #[test]
664    fn test_abstract_div_basic() {
665        let a = Interval::new(6, 12);
666        let b = Interval::new(2, 3);
667        let result = abstract_div(&a, &b);
668        assert!(result.lo >= 2 && result.hi <= 6);
669    }
670    #[test]
671    fn test_abstract_div_by_zero() {
672        let a = Interval::new(1, 10);
673        let b = Interval::new(-1, 1);
674        let result = abstract_div(&a, &b);
675        assert!(result.is_top());
676    }
677}
oxilean_kernel/abstract_interp/functions.rs

oxilean_kernel/abstract_interp/
functions.rs
