Use-after-free due to inlining

[mtzguido]

From this:

module Inline

module B = LowStar.Buffer
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32

let test (a : B.buffer U32.t) :
  HST.ST U32.t
    (requires fun h -> B.live h a /\ B.freeable a /\ B.length a > 0)
    (ensures fun _ _ _ -> True)
=
  [@@CInline] let x = B.index a 0ul in
  B.free a;
  x

I get the following C code, which is clearly wrong

/* 
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
  KaRaMeL invocation: ./karamel/krml Inline.krml -skip-compilation
  F* version: 7ecca72e
  KaRaMeL version: 97ced772
 */

#include "Inline.h"

uint32_t Inline_test(uint32_t *a)
{
  KRML_HOST_FREE(a);
  return a[0U];
}

@msprotz this is probably a bug in the inlining logic? I could take a look if it's not an obvious fix. I guess it could affect other projects.

Invocations below, just in case:

$ fstar.exe Inline.fst --codegen krml --extract '-*,Inline'
Extracted module Inline
Attempting to translate module Inline
* Warning 271 at /home/guido/r/gpu/main/FStar/ulib/FStar.UInt.fsti(435,8-435,51):
  - Pattern uses these theory symbols or terms that should not be in an SMT
    pattern:
      Prims.op_Subtraction

* Warning 241 at /home/guido/r/gpu/main/FStar/ulib/prims.fst(0,0-0,0):
  - Unable to load /home/guido/r/gpu/main/FStar/ulib/prims.fst.checked since
    checked file /home/guido/r/gpu/main/FStar/ulib/prims.fst.checked does not
    exist; will recheck /home/guido/r/gpu/main/FStar/ulib/prims.fst (suppressing
    this warning for further modules)

Verified module: Inline
All verification conditions discharged successfully

$ krml Inline.krml -skip-compilation
✔ [Monomorphization] ⏱️ 3ms
✔ [Inlining] ⏱️ 2ms
✔ [Pattern matches compilation] ⏱️ 2ms
✔ [Structs + Simplify 2] ⏱️ 4ms
✔ [Drop] ⏱️ <1ms
✔ [AstToCStar] ⏱️ <1ms
✔ [CStarToC] ⏱️ <1ms
⚙ KaRaMeL auto-detecting tools. Here's what we found:
readlink is: readlink
KaRaMeL called via: ./karamel/krml
KaRaMeL home is: /home/guido/r/karamel
⚙ KaRaMeL will drive F*. Here's what we found:
read FSTAR_HOME via the environment
fstar is on branch master
fstar is: /home/guido/r/fstar/master/bin/fstar.exe /home/guido/r/karamel/runtime/WasmSupport.fst /home/guido/r/fstar/master/ulib/FStar.UInt128.fst --trace_error --expose_interfaces --include /home/guido/r/karamel/krmllib --include /home/guido/r/karamel/include
✔ [PrettyPrinting] ⏱️ 4ms
KaRaMeL: wrote out .c files for Inline
KaRaMeL: wrote out .h files for Inline

[msprotz]

yes probably need to change the criterion is_readonly_pure_... to treat function calls as "unknown", although I'm surprised it doesn't do that -- let me know if you need more precise pointers, but I suspect there was an implicit assumption that was made that the only occurrences of this were for function arguments (of the form uu_) and that inlining never expected to reach this far down -- but now that has been broken with the addition of the attribute