Commits on Sep 7, 2022

1. [move-prover] preliminary support for type reflection …

   This commit introduces preliminary support on verifying code that
   uses reflection to obtain type information at runtime.
   
   We use a hyperthetical (and intrinsic) call
   `fun extension::type_info::type_name<T>(): String`
   that returns the type name of `T`.
   
   Being a pure function, this reflection function can be called
   from the spec context as well.
   
   In handling reflection, the high-level idea is:
   - if `T` is statically known when `type_name<T>` is called, replace this
     call with a constant
   - if `T` is unknown, full or partially, when this call is invoked,
     replace the `type_name` for `T` with a fresh variable
     `var #T_name: Vec int`, in particular:
     - if `T` is fully unknown, `type_name<T>` will be `#T_name`
     - if `T` is partially unknown (e.g., `type_name<vector<T>>`), then
       the `type_name` call will be replaced as
       `ConcatVec(ConcatVec("vector<", #T_name), ">")`
   
   This instrumentation happens at the translation phase, on the way to
   Boogie.

   

   meng-xu-cs committed Sep 7, 2022
   Configuration menu

   • View commit details
   • Copy full SHA for c9598cd
   • Browse repository at this point

   Copy the full SHA

   c9598cd View commit details

   Browse the repository at this point in the history