Open regehr opened 4 years ago
this is for @manasij7479 and @zhengyangl
alive2 does not understand phi nodes, so it cannot be used to double-check a synthesis result such as this one
regehr@home:~$ cat nop7.opt ; RUN: %souper-check -infer-rhs %s > %t1 ; RUN: %FileCheck %s < %t1 ; CHECK: Failed to infer RHS %0 = block 5 %1:i1 = var %2:i1 = var %3:i1 = or %1, %2 %4:i1 = phi %0, %1, %1, %1, %1, %1 infer %4 regehr@home:~$ ~/souper-regehr/build/souper-check -infer-rhs nop7.opt Dataflow Pruned 0/0 There are 2 Guesses ; RHS inferred successfully result %1 regehr@home:~$ ~/souper-regehr/build/souper-check -infer-rhs nop7.opt -souper-double-check souper-check: ../lib/Infer/AliveDriver.cpp:628: bool souper::AliveDriver::translateAndCache(const souper::Inst *, IR::Function &, souper::AliveDriver::Cache &): Assertion `false && "Phi with muliple arguments unimplemented"' failed. Aborted (core dumped) regehr@home:~$
Implemented
this is for @manasij7479 and @zhengyangl
alive2 does not understand phi nodes, so it cannot be used to double-check a synthesis result such as this one