Compiling the following strategy:

module proof1
imports libstrategolib predcalcrules
strategies
  main = io-wrap(eval)
  // eval = innermost(ImplicationToAndR) ; innermost(CommutativityEquiv)
  eval =  innermost(PredAndTrueR); PredAndTrue

and running it on:

Equiv(Equiv(And(Var("P"),Var("Q")),Var("P")),Equiv(Var("Q"),Or(Var("P"),Var("Q"))))

results in a segmentation fault:

$ ./proof1 < proof1.trm
Segmentation fault

In the stratego-shell, the same happens when manually applying the rules.

the relevant rules are:

module predcalcrules
imports PredCalc
rules
	ImplicationToAndR : Equiv(And(P,Q),P) -> Impl(P,Q)
	CommutativityEquiv : Equiv(P,Q)	-> Equiv(Q,P)
	PredAndTrue : And(P,Con("true")) -> P
	PredAndTrueR : P -> And(P,Con("true"))

removing innermost on the last line of the strategy does not result in a segmentation fault.

System details:

Linux 2.6.32-45-generic #104-Ubuntu SMP Tue Feb 19 21:20:09 UTC 2013 x86_64 GNU/Linux
aterm-2.5 (with longmax-patch), sdf2-bundle-2.4, strategoxt-0.17pre19210, stratego-shell-0.7pre17879

To compile stratego-shell, aterm-2.5 was listed as a dependency, and aterm-2.6 indeed does not work.

A GDB backtrace gives lines like the following, ad nauseam:

         :
#53390 0x00000000004011e9 in o_72 ()
#53391 0x00000000004011e9 in o_72 ()
#53392 0x00000000004011e9 in o_72 ()
#53393 0x00000000004011e9 in o_72 ()
#53394 0x00000000004011e9 in o_72 ()
#53395 0x00000000004011e9 in o_72 ()
#53396 0x00000000004011e9 in o_72 ()
        :

For general completeness, the signature:

module PredCalc

signature
  constructors
    Not   : Pred -> Pred
    Equiv : Pred * Pred -> Pred
    Impl  : Pred * Pred -> Pred
    Or    : Pred * Pred -> Pred
    And   : Pred * Pred -> Pred
    Con   : BoolConst -> Pred
    Var   : Id -> Pred
          : String -> BoolConst
          : String -> Id

Perhaps I am not using the strategies in the expected manner, but I hoped to see a more helpful error message in that case.

Submitted on 17 April 2013 at 21:48

The segmentation error that you obtain is caused by a stack overflow, suspicion which is confirmed by the repetitive entries in the stack trace you posted. This in turn is caused by infinite recursion in your main rule.

The infinite recursion is caused by the fact that application of PredAndTrueR always succeeds for any term. Innermost terminates when the argument strategy fails for all terms in the tree innermost is called on. Because the application of PredAndTrueR never fails, innermost never terminates, thus the infinite recursion. Innermost is a fixed-point traversal which repeatedly traverses the tree until a normal form is reached. In your case this fixed-point is never reached.

I hope this helps a bit with your current error.

Indeed the stack-trace is not very informative, this comes from the way the Stratego compiler works. In general when you get a segmentation fault and the stack is very repetitive either you have an infinite recursion or simply recursion is too deep and you’re running out of stack space.

Also, please note that the Stratego to C compiler is currently unmaintained. While most things work properly in the C version, I would strongly recommend using the Stratego to Java compiler which is actively maintained and which generates rather fast code.

I’m closing the issue now as this is not an error in the Stratego implementation itself. Please join the Stratego-users mailing list users@strategoxt.org which is dedicated to helping Stratego users.