From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!border1.nntp.ams1.giganews.com!nntp.giganews.com!newsfeed.xs4all.nl!newsfeed8.news.xs4all.nl!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Sat, 10 Dec 2016 00:32:40 +0200 Organization: Tidorum Ltd Message-ID: References: Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net sGDd7f+on5b5J406IBXjvgKkGq26cNsLOATvfdIp9qYVC/52EA Cancel-Lock: sha1:rG1XykEGlWuhrklVBFnQwozfOG0= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 In-Reply-To: Xref: news.eternal-september.org comp.lang.ada:32708 Date: 2016-12-10T00:32:40+02:00 List-Id: On 16-12-09 23:41 , Randy Brukardt wrote: > [I had to break the chain of replies as the headers got so long that the > message wouldn't post.] > > "Shark8" wrote in message > news:8e3b18a7-1e64-40bb-8d99-66fdeba58ace@googlegroups.com... >> On Tuesday, December 6, 2016 at 4:23:55 PM UTC-7, Randy Brukardt wrote: > ... >>> You seem to be assuming that it is practical to represent all kinds of >>> predicates as some sort of set. That's definitely not true; one of the >>> major >>> reasons that you can't use divide or mod in a static predicate is the >>> difficulty of representing the set. For instance, consider: >>> >>> subtype Even is new Natural with Dynamic_Predicate => Even mod 2 = >>> 0; >>> >>> If Natural is a 64 bit type, Even is a set of 2**63 items, no two are >>> contiguous. The representation of that is going to be a problem. One >>> could >>> imagine some special case to deal with this particular case, but then >>> there >>> are many other possible predicates with this property. >> >> Just because it's represented as a set doesn't mean that the set has to be >> represented as a bit-mask. (The obvious breaking example for that >> implementation here would be a string subtype constrained to contain only >> numeric characters.) > > In existing Ada implementations, sets are represented as a list of ranges. > (They come up in a number of places, including case statements and > Ada.Strings.) That's the expected implementation for any Ada set, but that > would take 2**63 items for Even. Static program analyzers, at least those analysing machine code and aiming to understand address alignments and aliasing, tend to need and use not only ranges, but ranges with strides (congruence information). The set of Even numbers would be easy and compact to represent in such a model, with stride = 2. Of course, it is a coincidence that Even happens to fit this model, and your general argument is not affected. > Trying to put a predicate logic prover into a compiler optimizer sounds > challenging at best. I'm a little surprised: I seem to remember that you have, earlier, said that you would like future compilers to prove all sorts of things about the program. But you were not thinking of predicate logic proofs? -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .