I'm trying to setup seahorn to statically analyze contracts, and seahorn does not like recursive functions. When compiling a test case to LLVM bitcode, some recursive functions appear, seemingly in the SCVal serialization code. @burnt solar is this expected?
#Recursive functions in XDR serialization code?
sour oracle
hearty olive
yes, SCVal is recursive by design as it needs to present arbitrary data structures (including recursive ones)
sour oracle
Okay, makes sense! Which ones in particular are recursive?
Btw, even if a structure is recursive, maybe the code handling it uses iteration
burnt solar
There are a few locations in the XDR, even outside new Soroban stuff, but they are all currently wrapped in an optional * in the XDR, so they are essentially union.
sour oracle
Loops are fine for my purpose
burnt solar
In Soroban the big one is ScVal.
ScVal contains ScVec that can contain ScVal.
There are other ScVal cases that do same.
sour oracle
Are you sure xdrgen actually generates recursive functions, or does it generate loops and maybe what I'm seeing comes from somewhere else?
burnt solar
But I'm pretty sure we have older cases that are in existing protocols.
... Sorry, I misread, are you concerned about recursive functiosn or recursive structures?
sour oracle
Recursive functions in the generated code
burnt solar
Could you point me to the function?
I wouldn't expect any of the functions to be recursive.
sour oracle
This function appears after compilation and is recursive: _ZN4core3ptr56drop_in_place$LT$stellar_xdr..next..generated..ScVal$GT$17h044a29ff334c2310E"(%"core::result::Result<stellar_xdr::next::generated::ScVal, raw_val::ConversionError>)
but maybe that's a destructor generated by the Rust compiler
burnt solar
Is the function name "drop_in_place"? I don't know how to read this syntax.
burnt solar
I quick grep suggests we are not calling it explicitly.
sour oracle
I guess it' likely: " For packed structs, this move is done automatically by the compiler."
ah no I'm misinterpreting that sentence
burnt solar
Do you have a stack trace that the call is in?
burnt solar
Hmm, assuming the second line is the return value of the function, it mentions raw_val::ConversionError, which is not in the xdrgen generated code. That's in the rs-soroban-env repo.
sour oracle
btw, I presume this is not an issue because we shouldn't be handling huge XDR objects, but just in case: https://github.com/rust-lang/rust/issues/58068
burnt solar
Interesting. @tacit prawn Fyi ☝🏻
tacit prawn
yeah, drop is recursive
I mean, any drop is a top-down destructuring of an object, drop-outer-object-then-drop-inner-objects, so it's recursive if the object has recursive structure (like scval)
theoretically drops could be organized by some mix of looping or tail calling in the sense that they don't return to the outer object once done with it, but I'd be surprised if anyone had tried to optimize that in reality
we could make a special sort of XDR-generating mode just for seahorn that implements drop manually (even trivially, by say leaking all of a value's substructure)