This is the mail archive of the gcc@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

Re: gcc compile time support for assumptions


Andrew Haley wrote:
Ian Lance Taylor writes:
> Abramo Bagnara <abramobagnara@tin.it> writes:
> > > I'd like to know if gcc has implemented some generic way to help
> > optimizer job by allowing programmers to specify assumptions (or
> > constraints).
> > The answer is no, there is nothing quite like you describe.
> > But I think it would be a good idea.


Something like this would greatly improve the code generation quality
of gcj.  There are a great many assertions that I could pass to VRP
and the optimizers: this is invariant, this is less than that, and so
on.

Note that such assertions also can function as predicates to be discharged in a proof engine. See work on SPARK (www.www.praxis-his.com).

One thing to consider here is whether to implement just a simple
assume as proposed, or a complete mechanism for pre and post
assertions (in particular, allowing you to talk about old values),
then it can serve as

a) a mechanism for programming by contract
b) a mechanism for interacting with proof tools
c) a mechanism to improve generated code as suggested in this thread

all at the same time

Eiffel should be examined for inspiration on such assertions.

Andrew.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]