Segfault when displaying a hole

[ohad]

Sorry this is a large program. I'm happy to try to cut it down to a minimal example, but I really have no clue where to start. If you have a suggestion, let me know.

Steps to Reproduce

Download segfaulting-frex.zip

$ unzip segfaulting-frex.zip 
Archive:  segfaulting-frex.zip
  inflating: Carriers.idr            
  inflating: Signatures.idr          
  inflating: Algebras.idr            
  inflating: Presentations.idr       
  inflating: Models.idr              
  inflating: Powers.idr              
  inflating: Frex.idr                
  inflating: Monoids.idr             
  inflating: CMonoids.idr            
$ idris2 CMonoids.idr 
1/9: Building Carriers (Carriers.idr)
2/9: Building Signatures (Signatures.idr)
3/9: Building Algebras (Algebras.idr)
4/9: Building Presentations (Presentations.idr)
5/9: Building Models (Models.idr)
6/9: Building Powers (Powers.idr)
7/9: Building Frex (Frex.idr)
8/9: Building Monoids (Monoids.idr)
9/9: Building CMonoids (CMonoids.idr)
Welcome to Idris 2 version 0.0.0.  Enjoy yourself!
CMonoids> :t zero_preservation

Expected Behavior

To display the context and expected type of the hole.

Observed Behavior

Segmentation fault (core dumped)

The offending hole zero_preservation is part of this definition (CMonoids.idr:133):

CMonoid_free_extend_zero_preservation
  : (n : Nat) -> (b : Model CMonoid_Th) 
  -> (f : Fin n -> U b) ->
    let a : Model CMonoid_Th
        a = Free_CMonoid_struct n                  in
    let h : Vect n Nat -> U b
        h = CMonoid_free_extend_struct n (Alg b) f in
    h ( algop _ (Alg a) CMONOID_ZERO) = algop _  (Alg b) CMONOID_ZERO
CMonoid_free_extend_zero_preservation n b f = 
  rewrite CMonoid_free_zero_representation n in
  ?zero_preservation

[ohad]

BTW, commenting out the rewrite before the ?zero_preservation and type-checking doesn't segfault.

[abailly]

Debugging idris2 gives me the following stack frame when it segfaults:

(lldb) bt 20
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=2, address=0x7ffeeebffe28)
  * frame #0: 0x0000000100043906 idris2`_idris__123_APPLY_95_0_125_ + 86
    frame #1: 0x00000001001c0a05 idris2`_idris_Utils_46_Binary_46_Core_46_TTC_46__64_Utils_46_Binary_46_TTC_36_Name_58__33_fromBuf_58_0 + 853
    frame #2: 0x00000001001c0c68 idris2`_idris_Utils_46_Binary_46_Core_46_TTC_46__64_Utils_46_Binary_46_TTC_36_Name_58__33_fromBuf_58_0 + 1464
    frame #3: 0x00000001001c0c68 idris2`_idris_Utils_46_Binary_46_Core_46_TTC_46__64_Utils_46_Binary_46_TTC_36_Name_58__33_fromBuf_58_0 + 1464
    frame #4: 0x00000001001c0c68 idris2`_idris_Utils_46_Binary_46_Core_46_TTC_46__64_Utils_46_Binary_46_TTC_36_Name_58__33_fromBuf_58_0 + 1464
    frame #5: 0x00000001001c0c68 idris2`_idris_Utils_46_Binary_46_Core_46_TTC_46__64_Utils_46_Binary_46_TTC_36_Name_58__33_fromBuf_58_0 + 1464
    frame #6: 0x00000001001c0c68 idris2`_idris_Utils_46_Binary_46_Core_46_TTC_46__64_Utils_46_Binary_46_TTC_36_Name_58__33_fromBuf_58_0 + 1464
    frame #7: 0x00000001001c0c68 idris2`_idris_Utils_46_Binary_46_Core_46_TTC_46__64_Utils_46_Binary_46_TTC_36_Name_58__33_fromBuf_58_0 + 1464
    frame #8: 0x00000001001c0c68 idris2`_idris_Utils_46_Binary_46_Core_46_TTC_46__64_Utils_46_Binary_46_TTC_36_Name_58__33_fromBuf_58_0 + 1464
    frame #9: 0x00000001001c0c68 idris2`_idris_Utils_46_Binary_46_Core_46_TTC_46__64_Utils_46_Binary_46_TTC_36_Name_58__33_fromBuf_58_0 + 1464

[ziman]

Segfaults in Idris generally mean stack overflow so it seems that something caused an infinite loop in the TTC deserialiser of names. Do you have outdated *.ttc/*.ttm files lying around from an old build of the standard library, perhaps? Idris2 loads things lazily so that's probably why the problem does not manifest until you inspect the hole.

[ohad]

Thanks! This problem does not necessarily have an infinite loop --- the proof terms are really big.

[edwinb]

The only plausible explanation I can come up with for a deeply nested name on reading (it turns out to be (NS [] (NS [] (NS [] ...))) is that there is some corruption in the .ttc file. Maybe something is being written incorrectly...

[ohad]

OK, so what's the best way to proceed?

[edwinb]

I believe I've found the cause of this. I encountered the same problem, but in an easier to reproduce way! There was an allocation error when writing out ttc files. I won't close this until someone (maybe me later) has tested this specific case though.