<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Aug 11, 2013, at 4:14 AM, "Nuno Lopes" <<a href="mailto:nunoplopes@sapo.pt">nunoplopes@sapo.pt</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><blockquote type="cite" style="font-family: monospace; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; ">This sounds promising. But we have some requirements that textbook rewriting systems can't handle:<br><br>- Expressions are DAGs, not trees.<br>- Targets can add custom rewriting rules and override standard rules.<br>- Rules will have predicates. Some predicates are static and only depend on the subtarget, some predicates will depend on the pattern being matched.<br>- The system won't be convergent if you ignore all the predicates.<br><br>So the question is, given those requirements, can we still prove termination?<br></blockquote><br style="font-family: monospace; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "><span style="font-family: monospace; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; display: inline !important; float: none; ">Uhm, I'm not sure about the custom target rules, since most likely a bunch of them will need to be specified in C++, and then they will be a black box to the tool..</span><br style="font-family: monospace; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "></blockquote><div><br></div><div>I think that SelectionDAG forces you to drop to C++ too soon, but we'll always need that possibility.</div><br><blockquote type="cite"><span style="font-family: monospace; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; display: inline !important; float: none; ">Regarding the predicates, how complicated are these? Aren't these expressions mostly in linear integer arithmetic? Or can you have arbitrary calls to complex C++ code?</span><br style="font-family: monospace; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "></blockquote></div><br><div>There are too many static predicates, so it isn't feasible to enumerate all possible combinations, but we can expose their relationships to the tool as boolean expressions. For example, X86 currently has:</div><div><br></div><div><div>def HasCMov : Predicate<"Subtarget->hasCMov()">;</div><div>def NoCMov : Predicate<"!Subtarget->hasCMov()">;</div><div><br></div></div><div>It would be simple to define:</div><div><br></div><div><div>def NoCMov : Predicate<(not HasCMov)>;</div></div><div><br></div><div>And the tool would be able to infer that the predicates are disjoint. Similarly:</div><div><br></div><div>def : Always<(or HasSSE1, (not HasSSE2))>;</div><div><br></div><div>can be used to infer an implication.</div><div><br></div><div>Many pattern predicates could be expressed in a DSL, but we should still make it possible to use C++ code.</div><div><br></div><div>Thanks,</div><div>/jakob</div><div><br></div></body></html>