Use addcons to prove relationship between input and output params

These constraints represent a minimized set of constraints needed to prove (approximately) that sub_001014fb.in_0.load <= sub_001014fb.out

The constraints are organized so that the transitive property just flows

Relating t320 to the out parameter:

τ320.load.σ64@0 ⊑ instr_00101544_0_$Uc000
instr_00101544_0_$Uc000 ⊑ instr_00101547_1_$Uc000
instr_00101547_1_$Uc000 ⊑ instr_00101434_0_RBP.store.σ64@-16
instr_00101434_0_RBP.store.σ64@-16 ⊑ sub_001014fb@RSP.σ64@-24
sub_001014fb@RSP.σ64@-24 ⊑ instr_00101434_0_RBP.load.σ64@-16
instr_00101434_0_RBP.load.σ64@-16 ⊑ instr_00101587_1_$Uc000
instr_00101587_1_$Uc000 ⊑ instr_00101587_2_RAX
instr_00101587_2_RAX ⊑ sub_001014fb.out

sub_001014fb.in_0 ⊑ instr_001016bd_0_RDI
sub_001014fb.in_0 ⊑ instr_0010176e_0_RDI
instr_001016bd_0_RDI ⊑ τ313
instr_0010176e_0_RDI ⊑ τ313
τ313 ⊑ instr_00101500_0_RBP.store.σ64@-24
instr_00101500_0_RBP.store.σ64@-24 ⊑ sub_001014fb@RSP.σ64@-32
sub_001014fb@RSP.σ64@-32 ⊑ instr_00101434_0_RBP.load.σ64@-24
instr_00101434_0_RBP.load.σ64@-24 ⊑ instr_0010153d_1_$Uc000

Add ties it together
Add(instr_0010153d_1_$Uc000,instr_00101535_1_RDX,τ320)

The point is we arent currently handling add constraints but the add constraint is the only thing currently tying together the in parameter to the out parameter. We need to apply these inference rules when inspecting the sketch graph: Screen Shot 2022-04-12 at 4 55 47 PM

It's tricky because this has to happen before simplification so we simplify out the relation, hopefully sketch building on unsimplified cons just works tm :)

trailofbits / binary_type_inference

Use addcons to prove relationship between input and output params #28