search

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
635 stars 42 forks source link

uc-crux-llvm: Panic on type alias with missing definition #710

Open langston-barrett opened 3 years ago

langston-barrett commented 3 years ago

Apparently, there's a reference to a type alias that isn't defined in this LLVM module. I didn't think this was possible, so uc-crux-llvm currently panics when it sees this.

cabal v2-run exe:uc-crux-llvm -- --config=conf.config --explore-budget=500 libcairo-script-interpreter.a.bc

conf.config:

explore: yes
re-explore: yes
explore-parallel: yes
explore-timeout: 5
no-compile: yes
goal-timeout: 3
timeout: 3
sim-verbose: 3
solver: "z3"
%< --------------------------------------------------- 
  Revision:  fb7ef34471d8b2471c2c79364d4cc8a9e2c24023
  Branch:    lb/translate-all-types (uncommited files present)
  Location:  asFullType
  Message:   Impossible: couldn't find definition for type alias
CallStack (from HasCallStack):
  panic, called at src/UCCrux/LLVM/Errors/Panic.hs:37:9 in uc-crux-llvm-0.1-inplace:UCCrux.LLVM.Errors.Panic
  panic, called at src/UCCrux/LLVM/FullType/Type.hs:433:7 in uc-crux-llvm-0.1-inplace:UCCrux.LLVM.FullType.Type
%< ---------------------------------------------------

libcairo-script-interpreter.a.bc.zip

langston-barrett commented 3 years ago

The type alias in question is struct._cairo, which is opaque:

%struct._cairo = type opaque
langston-barrett commented 3 years ago

I'm guessing the problem is here: https://github.com/GaloisInc/crucible/blob/6916feae5130703441c5aca7e2a1e057a438eb9f/uc-crux-llvm/src/UCCrux/LLVM/FullType/Type.hs#L253. In the process of recording FullType translations of type aliases, "inner" aliases are skipped. The solution is to iterate over the whole llvmAliasMap in the TypeContext and translate all type aliases, which makes sense to do as a follow-up to #708.