showcase/
showcase.rs

1use std::ops::{Add, Mul};
2use elina::ast::*;
3
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
showcase/showcase.rs

showcase/
showcase.rs
