Existe-t-il un analyseur statique Forth pour les effets de pile?

Question

Je perds de la productivité en raison d'erreurs de programmation qui provoquent un débordement de la pile. Par exemple, si j'omets un drop dans une branche IF ELSE THEN, dans une boucle, et que j'obtiens un débordement de pile, je dois généralement redémarrer mon environnement de développement. J'utilise SwapForth sur le iCEstick. Existe-t-il un analyseur statique qui prédit le résultat de pile d'un mot compilé?

Comme un outil automatisé qui vérifie que le code correspond toujours à la documentation (nnn nnn - f)?

Answer 1

Aucun outil de ce type ne m'est connu, mais pourquoi ne pas l'implémenter? Dans le cas général, le problème n'a pas de solution (voir Rice's theorem et halting problem). Néanmoins, un outil pratique pratique peut évidemment être mis en œuvre. Il peut s'agir d'un outil autonome ou d'une extension de votre système Forth particulier qui vérifie le code à la volée pendant la compilation. Comme pour un exemple, voir Forth Wizard de Peter Sovietov (2003). Cet outil évalue en interne l'effet de pile du code généré automatiquement. Un autre exemple: document Stack Verification par Rob Chapman (1997). Les articles suivants peuvent également être utiles: Inférence de type dans les langages à pile, Bill Stoddart et Peter J. Knaggs, 1992 (PDF); Inférence de type simple pour les langages orientés empilables d'ordre supérieur, Christopher Diggins, 2008 (PDF). La solution la plus simple consiste peut-être à vérifier dynamiquement l'effet de la pile (modification de la profondeur) et à déclencher une exception lorsque la signature de la pile est violée (dans les versions de développement uniquement). L'idée est de redéfinir : (et possible ;) pour obtenir l'effet de pile à partir du commentaire de la pile et de compiler l'emballage EXECUTE-BALANCED pour les définitions de deux-points.

: EXECUTE-EFFECT (i*x xt -- j*x n) 
    DEPTH 1- >R EXECUTE DEPTH R> - 
; 
: EXECUTE-BALANCED (i*x xt n -- j*x) \ j = i + n 
    >R EXECUTE-EFFECT R> = IF EXIT THEN 
    -5010 THROW \ stack is unbalanced 
; 

De toute évidence, une telle solution peut attraper une erreur seulement entre les mots, et il ne sera pas attraper un DROP manqué dans une boucle.