4 ms·

Yes gnatstack is neat, but, last time I tried (which was some time ago, I'll admit) there were some quite big limits and caveats with gnatstack analysis. The un

Yes gnatstack is neat, but, last time I tried (which was some time ago, I'll admit) there were some quite big limits and caveats with gnatstack analysis. The un precise analysis on second-stack, dynamic-sized object return, pointer-access calls (the last one being forbidden in spark?), and some others were quite blocking for my use cases.

MaxBarraclough 5y ago
Makes sense. The analysis will be downright impossible if you permit everything. Calls to arbitrary function pointers, or OOP dynamic-dispatch, for instance (unless these can be fully accounted for). I imagine it works well if you use MISRA C, which forbids function pointers. It looks like SPARK doesn't forbid function pointers, [0] although it bans plenty else. [1] I wonder if that's an issue for GNATstack. GNATstack is presumably mostly aimed at safety-critical code, as software in most other domains will be satisfied just relying on testing. Presumably, such codebases are likely to be using constrained language subsets anyway. [0] https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html#subprogram-pointers https://docs.adacore.com/spark2014-docs/html/ug/en/source/ac... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/source/language_restrictions.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/la...
- touisteur 5y ago
  Thanks for digging. I get there'd be limitations but I would prefer sometimes consistency: for gnatstack to support at least the SPARK subset (so, OOP, access to procedures, most 'reasonable' provable language features). I'm not faulting AdaCore, just noting the slight inconsistency, as I was disappointed first back then. I think it's a worthy space to improve though, because it's happened to me, on AoRTE (silver-level) SPARK, to crash because of an overeager parser. Fuzzing and more formal testing helps smoke some of those out but I'd like AoRTE to mean AoRTE :-) at least in no-dynamic-allocation-so-'new'-can't-fail scenarios. I'm guessing it's mostly 'no-one put a wad of cash thick enough on the table to have another look' which is understandable. I'll probably try to hit some corporate trouser pockets to start the engine again :-)
  - MaxBarraclough 5y ago
    > I would prefer sometimes consistency: for gnatstack to support at least the SPARK subset (so, OOP, access to procedures, most 'reasonable' provable language features) Again though this would require some way of enabling SPARK to track the stack-depth guarantees of every possible function that might be executed. Not to say it would be impossible, but I imagine it's far simpler for GNATstack to simply 'ban' function-pointers and dynamic dispatch. > it's happened to me, on AoRTE (silver-level) SPARK, to crash because of an overeager parser To be clear then this was deep recursion in a parser blowing the stack? Honestly I'm a little surprised SPARK even permits recursion in the first place. Seems like the 'safer' thing to do would be to forbid recursion and force the programmer to manually manage a stack data-structure (presumably one of fixed size). > I'm guessing it's mostly 'no-one put a wad of cash thick enough on the table to have another look' which is understandable I'm sure AdaCore are plenty motivated, but yes, no doubt they have only limited resources.
    - touisteur 5y ago
      Ah, a parser doesn't have to he recursive to blow the stack. Several layers of calls with lots of temporary arrays of large discriminated-record variables blew in my face, because of a misunderstanding about the size of some objects and not enough stack space reserved :-\. I wasn't thinking of asking the SPARK examiner/prover to prove stack size, more for gnatstack itself to support the full SPARK subset with precision. IIRC gnatstack used mostly -fstack-usage reports with a thick layer of post-processing, which can probably be improved with a layer of abstract interpretation handwave :-). I'll have to check the current state of affairs before I complain any more.

MaxBarraclough 5y ago

Makes sense. The analysis will be downright impossible if you permit everything. Calls to arbitrary function pointers, or OOP dynamic-dispatch, for instance (unless these can be fully accounted for). I imagine it works well if you use MISRA C, which forbids function pointers. It looks like SPARK doesn't forbid function pointers, [0] although it bans plenty else. [1] I wonder if that's an issue for GNATstack. GNATstack is presumably mostly aimed at safety-critical code, as software in most other domains will be satisfied just relying on testing. Presumably, such codebases are likely to be using constrained language subsets anyway. [0] https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html#subprogram-pointers https://docs.adacore.com/spark2014-docs/html/ug/en/source/ac... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/source/language_restrictions.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/la...

touisteur 5y ago
Thanks for digging. I get there'd be limitations but I would prefer sometimes consistency: for gnatstack to support at least the SPARK subset (so, OOP, access to procedures, most 'reasonable' provable language features). I'm not faulting AdaCore, just noting the slight inconsistency, as I was disappointed first back then. I think it's a worthy space to improve though, because it's happened to me, on AoRTE (silver-level) SPARK, to crash because of an overeager parser. Fuzzing and more formal testing helps smoke some of those out but I'd like AoRTE to mean AoRTE :-) at least in no-dynamic-allocation-so-'new'-can't-fail scenarios. I'm guessing it's mostly 'no-one put a wad of cash thick enough on the table to have another look' which is understandable. I'll probably try to hit some corporate trouser pockets to start the engine again :-)
- MaxBarraclough 5y ago
  > I would prefer sometimes consistency: for gnatstack to support at least the SPARK subset (so, OOP, access to procedures, most 'reasonable' provable language features) Again though this would require some way of enabling SPARK to track the stack-depth guarantees of every possible function that might be executed. Not to say it would be impossible, but I imagine it's far simpler for GNATstack to simply 'ban' function-pointers and dynamic dispatch. > it's happened to me, on AoRTE (silver-level) SPARK, to crash because of an overeager parser To be clear then this was deep recursion in a parser blowing the stack? Honestly I'm a little surprised SPARK even permits recursion in the first place. Seems like the 'safer' thing to do would be to forbid recursion and force the programmer to manually manage a stack data-structure (presumably one of fixed size). > I'm guessing it's mostly 'no-one put a wad of cash thick enough on the table to have another look' which is understandable I'm sure AdaCore are plenty motivated, but yes, no doubt they have only limited resources.
  - touisteur 5y ago
    Ah, a parser doesn't have to he recursive to blow the stack. Several layers of calls with lots of temporary arrays of large discriminated-record variables blew in my face, because of a misunderstanding about the size of some objects and not enough stack space reserved :-\. I wasn't thinking of asking the SPARK examiner/prover to prove stack size, more for gnatstack itself to support the full SPARK subset with precision. IIRC gnatstack used mostly -fstack-usage reports with a thick layer of post-processing, which can probably be improved with a layer of abstract interpretation handwave :-). I'll have to check the current state of affairs before I complain any more.