Lambda the Ultimate

When I first learned Scheme I had heard about how powerful the macro system was, and that the full power of the language was available during the macro system.

What I think is interesting was an assumption I had before I learned how the macro system actually works. I had assumed that one could call functions during macro expansion that were defined in the source program.

I am trying to find out whether such macro systems actually exist, where the AST is evaluated as needed while it is being transformed. One simple approach I can imagine, is that when a macro uses a function defined in the source, that function is evaluated/compiled as needed. If it contains macros that haven't been expanded into something meaningful, then the compiler simply fails.

I think this kind of system where macros are intertwined with a program interpreter, may be hard to reason about formally, but could be a very expressive tool.

Has anyone encountered such a macro system?

We discuss the problem of path feasibility for programs manipulating strings using a collection of standard string library functions. We prove results on the complexity of this problem, including its undecidability in the general case and decidability of some special cases. In the context of test-case generation, we are interested in an efficient finite model finding method for string constraints. To this end we develop a two-tier finite model finding procedure. First, an integer abstraction of string constraints are passed to an SMT (Satisfiability Modulo Theories) solver. The abstraction is either unsatisfiable, or the solver produces a model that fixes lengths of enough strings to reduce the entire problem to be finite domain. The resulting fixed-length string constraints are then solved in a second phase. We implemented the procedure in a symbolic execution framework, report on the encouraging results and discuss directions for improving the method further.

The authors note that while strings are a fundamental data type, the main existing way of handling strings in symbolic test-case generation tools is to treat them as regular arrays, and to treat string library subroutines as regular procedure calls, thus turning even simple calls to library functions into loop constructs.