Goose  Artifact [9709b5c060]

Artifact 9709b5c060c38aad615b59327919103279704b28ac3bd347d21ce84978b0cb73:

  • File bs/builtins/types/propositions/drop.cpp — part of check-in [68260b65f2] at 2022-03-14 19:23:09 on branch trunk —
    • bracket blocks inlined in the code are no longer proposition lists but a new type of block to contain "ghost code" (ie a verification specific cfg)
    • added a GhostBranch instruction to insert the above in the middle of regular code
    • removed a bunch of hacks to ignore load/stores involving ghost funcs during execution and codegen since they are now separated from normal code using the above
    • miscellaneous other refactorings and improvements
    • as a result ghost code is now more flexible and can use idiomatic tuple assignments to exchange the values of two ghost function closures
    (user: zlodo size: 1254)

#include "builtins/builtins.h"
#include "parse/parse.h"

using namespace goose::parse;
using namespace goose::cir;

namespace goose::builtins
{
    void SetupPropositionsDropValue( Env& e )
    {
        // When a boolean is dropped into Propositions, it is appended as a new proposition.
        RegisterBuiltinFunc< Intrinsic< void ( TypeWrapper< ptr< Propositions > >, bool ) > >( e, e.extDropValue(),
            []( const Context& c, const Value& p, const Value& v )
            {
                auto props = *FromValue< TypeWrapper< ptr< Propositions > > >( p );
                props->append( v );
            } );

        // When anything else is dropped into Propositions, complain if we're only supposed
        // to have bools.
        RegisterBuiltinFunc< Intrinsic< void ( TypeWrapper< ptr< Propositions > >, Value ) > >( e, e.extDropValue(),
            []( const Context& c, const Value& p, const Value& v )
            {
                auto props = *FromValue< TypeWrapper< ptr< Propositions > > >( p );
                props->poison();

                DiagnosticsManager::GetInstance().emitErrorMessage( v.locationId(),
                    "only boolean expressions are allowed in proposition lists.", 0 );
            } );
    }
}