Goose  Check-in [c3f897359f]

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:
  • Got rid of the gross system of performing unifications twice in all cases. It's only really needed when invoking template functions.
  • Since the above had the unexpected side effect of fixing the tuple Initialize() overloads not being called, fixed those (which were actually broken).
Downloads: Tarball | ZIP archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA3-256: c3f897359f35531163f9b28cd9bd735f0e82e289a97629a10f7ca376b0d7bc50
User & Date: achavasse 2020-06-20 14:32:02.342
Context
2020-06-20
16:07
Fixed one of the tuple unification rule. check-in: 48bb81ebdd user: achavasse tags: trunk
14:32
  • Got rid of the gross system of performing unifications twice in all cases. It's only really needed when invoking template functions.
  • Since the above had the unexpected side effect of fixing the tuple Initialize() overloads not being called, fixed those (which were actually broken).
 check-in: c3f897359f user: achavasse tags: trunk
2020-06-15
22:09
Refactored the integer/ct_int unification to defer the size/sign check to a postprocessing callback. check-in: ac4e681af3 user: achavasse tags: trunk
Changes
Unified Diff Ignore Whitespace Patch
Changes to .fossil-settings/ignore-glob. 
1
2
3
4
5
6
7
8


file-*
ci-comment-*
*-baseline
*-merge
*-original
build
subprojects/*/*
tools/vscode-extension/vscode-extension










>

1
2
3
4
5
6
7
8
9

file-*
ci-comment-*
*-baseline
*-merge
*-original
build
subprojects/*/*
tools/vscode-extension/vscode-extension
builddir
Changes to bs/builtins/types/constrainedfunc/invoke.cpp. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19



20
21
22
23


24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

#include "builtins/builtins.h"

using namespace goose::sema;

namespace goose::builtins
{
    class ConstrainedFuncInvocationRule : public InvocationRule
    {
        public:
            Value resolveInvocation( const Context& c, uint32_t loc, const Value& callee, const Value& args ) const final
            {
                auto callPat = VEC( c.domain(), args.val(), HOLE( "_"_sid ) );

                // Unify with the constraint pattern. We only care that there is at least one
                // solution, and if so, we defer the actual call resolution to the contained
                // function.
                auto cfunc = FromValue< ConstrainedFunc >( callee );
                assert( cfunc );




                auto g = FullUnify( cfunc->constraintPat(), callPat, c );

                auto it = g.begin();
                if( it == g.end() )


                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "function arguments mismatch." );
                    return PoisonValue();
                }

                return cfunc->invRule()->resolveInvocation( c, loc, cfunc->func(), args );
            }
    };

    void SetupConstrainedFuncInvocationRule( Env& e )
    {
        e.invocationRuleSet()->addRule(
            ValueToIRExpr( Value(










|

|







>
>
>
|
|
<
|
>
>
|
|
|
|
|
<
<
<








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

25
26
27
28
29
30
31
32



33
34
35
36
37
38
39

#include "builtins/builtins.h"

using namespace goose::sema;

namespace goose::builtins
{
    class ConstrainedFuncInvocationRule : public InvocationRule
    {
        public:
            Value resolveInvocation( const Context& c, uint32_t loc, const Value& callee, const Term& args ) const final
            {
                auto callPat = VEC( c.domain(), args, HOLE( "_"_sid ) );

                // Unify with the constraint pattern. We only care that there is at least one
                // solution, and if so, we defer the actual call resolution to the contained
                // function.
                auto cfunc = FromValue< ConstrainedFunc >( callee );
                assert( cfunc );

                UnificationContext uc( c );
                uc.setComplexity( GetComplexity( cfunc->constraintPat() ) + GetComplexity( callPat ) );

                for( auto&& [s, uc] : Unify( cfunc->constraintPat(), callPat, uc ) )
                {

                    if( Postprocess( s, uc ) )
                        return cfunc->invRule()->resolveInvocation( c, loc, cfunc->func(), args );
                }

                // TODO display details
                DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                    "function arguments mismatch." );
                return PoisonValue();



            }
    };

    void SetupConstrainedFuncInvocationRule( Env& e )
    {
        e.invocationRuleSet()->addRule(
            ValueToIRExpr( Value(
︙︙
Changes to bs/builtins/types/constrainedfunc/unify.cpp.
︙︙
91
92
93
94
95
96
97

























98
99

            auto it = g.begin();
            if( it != g.end() )
            {
                auto func = ValueToIRExpr( cfunc->func() );
                co_yield Unify( lhs, func, uc );
            }
        } );

























    }
}








>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>



91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124

            auto it = g.begin();
            if( it != g.end() )
            {
                auto func = ValueToIRExpr( cfunc->func() );
                co_yield Unify( lhs, func, uc );
            }
        } );

        // constrainedfunc param / any arg:
        // Just yield the constrained func.
        //
        // This is because when we monomorphize a function that takes
        // a polymorphic function type, we turn the later into a
        // compile time constant. So it isn't really a parameter
        // in the resulting monomorphic function, and we just want
        // to ignore whatever parameter is being passed there
        e.unificationRuleSet()->addSymRule( URINFOS,

            ValueToIRExpr( ValuePattern(
                TSID( constant ),
                GetValueType< builtins::ConstrainedFunc >(),
                ANYTERM( _ ) ) ),

            ValueToIRExpr( ValuePattern(
                ANYTERM( _ ),
                ANYTERM( _ ),
                ANYTERM( _ ) ) ),

        []( const Term& lhs, const Term& rhs, const UnificationContext& uc ) -> UniGen
        {
            co_yield { lhs, uc };
        } );
    }
}
Changes to bs/builtins/types/func/invoke.cpp. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

#include "builtins/builtins.h"

using namespace goose::sema;

namespace goose::builtins
{
    class FunctionInvocationRule : public InvocationRule
    {
        public:
            Value resolveInvocation( const Context& c, uint32_t loc, const Value& callee, const Value& args ) const final
            {
                optional< UnificationContext > bestUC;
                optional< Term > bestSol;
                bool ambiguous = false;
                auto sig = GetFuncSig( callee );

                auto callPat = VEC( c.domain(), args.val(), HOLE( "_"_sid ) );

                auto us = FindBestUnification( sig, callPat, c );

                if( holds_alternative< NoUnification >( us ) )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,










|






|








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

#include "builtins/builtins.h"

using namespace goose::sema;

namespace goose::builtins
{
    class FunctionInvocationRule : public InvocationRule
    {
        public:
            Value resolveInvocation( const Context& c, uint32_t loc, const Value& callee, const Term& args ) const final
            {
                optional< UnificationContext > bestUC;
                optional< Term > bestSol;
                bool ambiguous = false;
                auto sig = GetFuncSig( callee );

                auto callPat = VEC( c.domain(), args, HOLE( "_"_sid ) );

                auto us = FindBestUnification( sig, callPat, c );

                if( holds_alternative< NoUnification >( us ) )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
︙︙
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "ambiguous function call." );
                    return PoisonValue();
                }

                auto&& [s,uc] = get< UniSol >( us );

                return invoke( c, loc, callee, s, uc );
            }

            Value invoke( const Context& c, uint32_t loc, const Value& callee, const Term& unifiedCallPat, UnificationContext& uc ) const final
            {
                auto newCallee = prepareFunc( c, 0, callee, unifiedCallPat, uc );
                if( newCallee.isPoison() )
                    return PoisonValue();

                auto callDecomp = Decompose( unifiedCallPat,
                    Vec(








|


|








32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "ambiguous function call." );
                    return PoisonValue();
                }

                auto&& [s,uc] = get< UniSol >( us );

                return invoke( c, loc, callee, args, s, uc );
            }

            Value invoke( const Context& c, uint32_t loc, const Value& callee, const Term& args, const Term& unifiedCallPat, UnificationContext& uc ) const final
            {
                auto newCallee = prepareFunc( c, 0, callee, unifiedCallPat, uc );
                if( newCallee.isPoison() )
                    return PoisonValue();

                auto callDecomp = Decompose( unifiedCallPat,
                    Vec(
︙︙
Changes to bs/builtins/types/localvar/invoke.cpp.
︙︙
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27


                auto val = BuildComputedValue( lv.type(),
                    llr::Load( llr::VarAddress( lv.index() ), lv.type() ) );

                return sema::CanBeInvoked( c, val );
            }

            Value resolveInvocation( const Context& c, uint32_t locationId, const Value& callee, const Value& args ) const final
            {
                auto lv = *FromValue< LocalVar >( callee );

                auto val = BuildComputedValue( lv.type(),
                    llr::Load( llr::VarAddress( lv.index() ), lv.type() ) );

                return sema::GetInvocationRule( *c.env(), val )->resolveInvocation( c, locationId, val, args );








|








13
14
15
16
17
18
19
20
21
22
23
24
25
26
27


                auto val = BuildComputedValue( lv.type(),
                    llr::Load( llr::VarAddress( lv.index() ), lv.type() ) );

                return sema::CanBeInvoked( c, val );
            }

            Value resolveInvocation( const Context& c, uint32_t locationId, const Value& callee, const Term& args ) const final
            {
                auto lv = *FromValue< LocalVar >( callee );

                auto val = BuildComputedValue( lv.type(),
                    llr::Load( llr::VarAddress( lv.index() ), lv.type() ) );

                return sema::GetInvocationRule( *c.env(), val )->resolveInvocation( c, locationId, val, args );
︙︙
Changes to bs/builtins/types/overloadset/invoke.cpp. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19


20
21



22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39








40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64

#include "builtins/builtins.h"

using namespace goose::sema;

namespace goose::builtins
{
    class OverloadSetInvocationRule : public InvocationRule
    {
        public:
            Value resolveInvocation( const Context& c, uint32_t loc, const Value& callee, const Value& args ) const final
            {
                auto pOvlSet = *FromValue< ptr< OverloadSet > >( callee );

                optional< UnificationContext > bestUC;
                optional< Term > bestSol;
                const OverloadSet::Overload* bestOvl = nullptr;
                bool ambiguous = false;

                auto rtPat = HOLE( "_"_sid );


                for( auto&& [s,ovl,uc] : pOvlSet->fullUnify( c.domain(), args.val(), rtPat, c ) )
                {



                    if( bestSol && uc.score() < bestUC->score() )
                        continue;

                    auto pps = Postprocess( s, uc );
                    if( !pps )
                        continue;

                    if( uc.score() == bestUC->score() )
                    {
                        ambiguous = true;
                        continue;
                    }

                    bestUC = uc;
                    bestSol = move( *pps );
                    bestOvl = &ovl;
                    ambiguous = false;
                }









                if( !bestSol )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "function arguments mismatch." );
                    return PoisonValue();
                }

                if( ambiguous )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "ambiguous function call." );
                    return PoisonValue();
                }

                return bestOvl->pInvRule->invoke( c, loc, *bestOvl->callee, *bestSol, *bestUC );
            }
    };

    ptr< InvocationRule >& GetOverloadSetInvocationRule()
    {
        static ptr< InvocationRule > pRule = make_shared< OverloadSetInvocationRule >();
        return pRule;










|









>
>
|

>
>
>
|






|










>
>
>
>
>
>
>
>









<
<
<
<
<
<
<
<
|








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61








62
63
64
65
66
67
68
69

#include "builtins/builtins.h"

using namespace goose::sema;

namespace goose::builtins
{
    class OverloadSetInvocationRule : public InvocationRule
    {
        public:
            Value resolveInvocation( const Context& c, uint32_t loc, const Value& callee, const Term& args ) const final
            {
                auto pOvlSet = *FromValue< ptr< OverloadSet > >( callee );

                optional< UnificationContext > bestUC;
                optional< Term > bestSol;
                const OverloadSet::Overload* bestOvl = nullptr;
                bool ambiguous = false;

                auto rtPat = HOLE( "_"_sid );
                UnificationContext uc( c );

                for( auto&& [s,ovl,uc] : pOvlSet->unify( c.domain(), args, rtPat, uc ) )
                {
                    if( uc.numUnknownValues() )
                       continue;

                    if( bestUC && uc.score() < bestUC->score() )
                        continue;

                    auto pps = Postprocess( s, uc );
                    if( !pps )
                        continue;

                    if( bestUC && uc.score() == bestUC->score() )
                    {
                        ambiguous = true;
                        continue;
                    }

                    bestUC = uc;
                    bestSol = move( *pps );
                    bestOvl = &ovl;
                    ambiguous = false;
                }

                if( ambiguous )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "ambiguous function call." );
                    return PoisonValue();
                }

                if( !bestSol )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "function arguments mismatch." );
                    return PoisonValue();
                }









                return bestOvl->pInvRule->invoke( c, loc, *bestOvl->callee, args, *bestSol, *bestUC );
            }
    };

    ptr< InvocationRule >& GetOverloadSetInvocationRule()
    {
        static ptr< InvocationRule > pRule = make_shared< OverloadSetInvocationRule >();
        return pRule;
︙︙
Changes to bs/builtins/types/template/invoke.cpp. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

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

using namespace goose::sema;
using namespace goose::parse;

namespace goose::builtins
{
    class TemplateFunctionInvocationRule : public InvocationRule
    {
        public:
            Value resolveInvocation( const Context& c, uint32_t loc, const Value& callee, const Value& args ) const final
            {
                auto tf = FromValue< TFunc >( callee );
                assert( tf );

                optional< UnificationContext > bestUC;
                optional< Term > bestSol;
                bool ambiguous = false;

                auto callPat = VEC( c.domain(), args.val(), HOLE( "_"_sid ) );
                auto us = FindBestUnification( tf->signature(), callPat, c );

                if( holds_alternative< NoUnification >( us ) )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "template function arguments mismatch." );
                    return PoisonValue();
                }

                if( holds_alternative< AmbiguousUnification >( us ) )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "ambiguous function call." );
                    return PoisonValue();
                }

                auto&& [s,uc] = get< UniSol >( us );

                return invoke( c, loc, callee, s, uc );
            }

            Value invoke( const Context& c, uint32_t loc, const Value& callee, const Term& unifiedCallPat, UnificationContext& uc ) const final
            {
                auto callDecomp = Decompose( unifiedCallPat,
                    Vec(
                        SubTerm(),  // domain
                        SubTerm(),  // args
                        SubTerm()   // return type
                    )
                );

                auto&& [domain, unifiedArgs, unifiedRType] = *callDecomp;

                DiagnosticsContext dc( loc, loc ?  "Called here." : "", false );

                auto instanceFunc = InstantiateTFunc( c, callee, unifiedCallPat, uc );
                if( instanceFunc.isPoison() )
                    return PoisonValue();

                auto ft = *FromValue< FuncType >( *ValueFromIRExpr( instanceFunc.type() ) );
                auto argList = BuildArgListForCall( ft, unifiedArgs );

                return BuildComputedValue( unifiedRType, llr::Call( instanceFunc, argList ) );
            }

            optional< Term > getSignature( const Value& callee ) const final
            {
                auto tfuncVal = FromValue< TFunc >( callee );
                assert( tfuncVal );
                return tfuncVal->signature();












|








|




















|


|

















<
<
|
<








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62


63

64
65
66
67
68
69
70

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

using namespace goose::sema;
using namespace goose::parse;

namespace goose::builtins
{
    class TemplateFunctionInvocationRule : public InvocationRule
    {
        public:
            Value resolveInvocation( const Context& c, uint32_t loc, const Value& callee, const Term& args ) const final
            {
                auto tf = FromValue< TFunc >( callee );
                assert( tf );

                optional< UnificationContext > bestUC;
                optional< Term > bestSol;
                bool ambiguous = false;

                auto callPat = VEC( c.domain(), args, HOLE( "_"_sid ) );
                auto us = FindBestUnification( tf->signature(), callPat, c );

                if( holds_alternative< NoUnification >( us ) )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "template function arguments mismatch." );
                    return PoisonValue();
                }

                if( holds_alternative< AmbiguousUnification >( us ) )
                {
                    // TODO display details
                    DiagnosticsManager::GetInstance().emitErrorMessage( loc,
                        "ambiguous function call." );
                    return PoisonValue();
                }

                auto&& [s,uc] = get< UniSol >( us );

                return invoke( c, loc, callee, args, s, uc );
            }

            Value invoke( const Context& c, uint32_t loc, const Value& callee, const Term& args, const Term& unifiedCallPat, UnificationContext& uc ) const final
            {
                auto callDecomp = Decompose( unifiedCallPat,
                    Vec(
                        SubTerm(),  // domain
                        SubTerm(),  // args
                        SubTerm()   // return type
                    )
                );

                auto&& [domain, unifiedArgs, unifiedRType] = *callDecomp;

                DiagnosticsContext dc( loc, loc ?  "Called here." : "", false );

                auto instanceFunc = InstantiateTFunc( c, callee, unifiedCallPat, uc );
                if( instanceFunc.isPoison() )
                    return PoisonValue();



                return GetFuncInvocationRule()->resolveInvocation( c, loc, instanceFunc, args );

            }

            optional< Term > getSignature( const Value& callee ) const final
            {
                auto tfuncVal = FromValue< TFunc >( callee );
                assert( tfuncVal );
                return tfuncVal->signature();
︙︙
Changes to bs/builtins/types/tuple/init.cpp. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

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

using namespace goose::parse;
using namespace goose::llr;

namespace goose::builtins
{
    void SetupTupleInitialize( Env& e )
    {
        // TODO: tuple non default initialization. It could be implemented right now with some hacks
        // but I prefer to wait until after varag templates are implemented and do it right.

        // Tuples default initialization: attempt to default initialize every element.
        RegisterBuiltinFunc< Intrinsic< void (
                CustomPattern< Reference, Reference::PatternMutable< TuplePattern > >
                ) > >( e, e.extInitialize(),
            []( const Context& c, const Value& tupRef )
            {
                auto ref = *FromValue< Reference >( tupRef );











<
<
<








1
2
3
4
5
6
7
8
9
10



11
12
13
14
15
16
17

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

using namespace goose::parse;
using namespace goose::llr;

namespace goose::builtins
{
    void SetupTupleInitialize( Env& e )
    {



        // Tuples default initialization: attempt to default initialize every element.
        RegisterBuiltinFunc< Intrinsic< void (
                CustomPattern< Reference, Reference::PatternMutable< TuplePattern > >
                ) > >( e, e.extInitialize(),
            []( const Context& c, const Value& tupRef )
            {
                auto ref = *FromValue< Reference >( tupRef );
︙︙
32
33
34
35
36
37
38
39
40




41
42
43
44
45
46
47

                    addr.appendToPath( index++ );

                    auto elemRef = BuildComputedValue( ValueToIRExpr( ToValue( rt ) ),
                        Load( move( addr ), rt.type() ) )
                        .setLocationId( elemType.locationId() );

                    DiagnosticsContext dc( elemType.locationId(), "When invoking Initialize." );
                    InvokeOverloadSet( c, c.env()->extInitialize(),
                        MakeTuple( elemRef ) );





                    return true;
                } );
            } );


        // Tuples initialization: intialize each element with the corresponding element








|

>
>
>
>








29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

                    addr.appendToPath( index++ );

                    auto elemRef = BuildComputedValue( ValueToIRExpr( ToValue( rt ) ),
                        Load( move( addr ), rt.type() ) )
                        .setLocationId( elemType.locationId() );

                    DiagnosticsContext dc( elemType.locationId(), "When invoking Initialize." );
                    auto init = InvokeOverloadSet( c, c.env()->extInitialize(),
                        MakeTuple( elemRef ) );

                    DiagnosticsContext dc2( elemType.locationId(), "When invoking DropValue." );
                     InvokeOverloadSet( c, c.env()->extDropValue(),
                        MakeTuple( init ) );

                    return true;
                } );
            } );


        // Tuples initialization: intialize each element with the corresponding element
︙︙
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94




95
96
97
98
99
100

                {
                    auto elemType = *ValueFromIRExpr( t );
                    auto initType = *ValueFromIRExpr( i );

                    // Create a mutable reference to the element to initialize
                    ReferenceType rt( t, TSID( mut ) );
                    auto addr = lref.address();
                    addr.appendToPath( index++ );

                    auto elemRef = BuildComputedValue( ValueToIRExpr( ToValue( rt ) ),
                        Load( move( addr ), rt.type() ) )
                        .setLocationId( elemType.locationId() );

                    // Create a reference to the element to initialize, that have the same behavior as the original
                    // reference to the initializer tuple.
                    ReferenceType irt( i, rref.type().behavior() );
                    auto initAddr = rref.address();
                    initAddr.appendToPath( index++ );

                    auto initRef = BuildComputedValue( ValueToIRExpr( ToValue( irt ) ),
                        Load( move( initAddr ), irt.type() ) )
                        .setLocationId( initType.locationId() );

                    DiagnosticsContext dc( elemType.locationId(), "When invoking Initialize." );
                    InvokeOverloadSet( c, c.env()->extInitialize(),
                        MakeTuple( elemRef, initRef ) );





                    return true;
                } );
            } );
    }
}








|
















|

>
>
>
>







70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

                {
                    auto elemType = *ValueFromIRExpr( t );
                    auto initType = *ValueFromIRExpr( i );

                    // Create a mutable reference to the element to initialize
                    ReferenceType rt( t, TSID( mut ) );
                    auto addr = lref.address();
                    addr.appendToPath( index );

                    auto elemRef = BuildComputedValue( ValueToIRExpr( ToValue( rt ) ),
                        Load( move( addr ), rt.type() ) )
                        .setLocationId( elemType.locationId() );

                    // Create a reference to the element to initialize, that have the same behavior as the original
                    // reference to the initializer tuple.
                    ReferenceType irt( i, rref.type().behavior() );
                    auto initAddr = rref.address();
                    initAddr.appendToPath( index++ );

                    auto initRef = BuildComputedValue( ValueToIRExpr( ToValue( irt ) ),
                        Load( move( initAddr ), irt.type() ) )
                        .setLocationId( initType.locationId() );

                    DiagnosticsContext dc( elemType.locationId(), "When invoking Initialize." );
                    auto init = InvokeOverloadSet( c, c.env()->extInitialize(),
                        MakeTuple( elemRef, initRef ) );

                    DiagnosticsContext dc2( elemType.locationId(), "When invoking DropValue." );
                     InvokeOverloadSet( c, c.env()->extDropValue(),
                        MakeTuple( init ) );

                    return true;
                } );
            } );
    }
}
Changes to bs/execute/vm.cpp.
︙︙
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197

        return PoisonValue();

    return ValueFromIRExpr( **pTerm );
}

optional< Value > VM::execute( const llr::AllocVar& av )
{
    m_frame.setTemporary( av.index(), Term() );
    return nullopt;
}

optional< Value > VM::execute( const llr::Load& l )
{
    const auto* addr = calcAddress( l.addr() );
    if( !addr )
        return nullopt;

    return ValueFromIRExpr( *addr );
}

optional< Value > VM::execute( const llr::Store& s )
{
    auto* addr = calcAddress( s.addr() );
    if( !addr )
        return nullopt;

    auto result = Evaluate( s.val(), *this );
    if( !result.isConstant() )
        result = PoisonValue();

    *addr = ValueToIRExpr( result );
    return nullopt;
}

optional< Value > VM::execute(
    const llr::Phi& p )
{
    p.forAllIncomings( [&]( auto&& bb, auto&& val )
    {
        if( bb == m_pPreviousBB )
        {
            m_frame.setTemporary( p.destIndex(), ValueToIRExpr( Evaluate( val, *this ) ) );
            return false;








|




















|





|
<








155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189

190
191
192
193
194
195
196

        return PoisonValue();

    return ValueFromIRExpr( **pTerm );
}

optional< Value > VM::execute( const llr::AllocVar& av )
{
    m_frame.setTemporary( av.index(), BuildUninitializedValue( av.type() ) );
    return nullopt;
}

optional< Value > VM::execute( const llr::Load& l )
{
    const auto* addr = calcAddress( l.addr() );
    if( !addr )
        return nullopt;

    return ValueFromIRExpr( *addr );
}

optional< Value > VM::execute( const llr::Store& s )
{
    auto* addr = calcAddress( s.addr() );
    if( !addr )
        return nullopt;

    auto result = Evaluate( s.val(), *this );
    if( !result.isConstant() )
        return PoisonValue();

    *addr = ValueToIRExpr( result );
    return nullopt;
}

optional< Value > VM::execute( const llr::Phi& p )

{
    p.forAllIncomings( [&]( auto&& bb, auto&& val )
    {
        if( bb == m_pPreviousBB )
        {
            m_frame.setTemporary( p.destIndex(), ValueToIRExpr( Evaluate( val, *this ) ) );
            return false;
︙︙
327
328
329
330
331
332
333


















{
    auto* optPTerm = m_frame.getTemporary( va.index );
    if( !optPTerm )
        return nullptr;

    return &( **optPTerm );
}

























>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>

326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349

{
    auto* optPTerm = m_frame.getTemporary( va.index );
    if( !optPTerm )
        return nullptr;

    return &( **optPTerm );
}

Term VM::BuildUninitializedValue( const Value& type )
{
    if( !IsTupleType( type ) )
        return TSID( UNINITIALIZED );

    auto tupContent = make_shared< Vector >();
    tupContent->reserve( TupleTypeSize( type ) );

    ForEachInTupleType( type, [&]( auto&& t )
    {
        tupContent->append( BuildUninitializedValue( *ValueFromIRExpr( t ) ) );
        return true;
    } );

    return ValueToIRExpr( Value( ValueToIRExpr( type ), TERM( move( tupContent ) ) ) );
}
Changes to bs/execute/vm.h.
︙︙
67
68
69
70
71
72
73

74
75
76
77
78
79
80

            ptr< BasicBlock > executeTerminator( const T& )
            {
                return nullptr;
            }

        private:
            static optional< Value > ExecuteBuiltinFuncCall( const Value& func, const Term& args );


            template< typename F >
            Value executeEqualityBinOp( const llr::BinaryOp& bo, F&& func );

            template< typename F >
            Value executeLogicBinOp( const llr::BinaryOp& bo, F&& func );









>








67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

            ptr< BasicBlock > executeTerminator( const T& )
            {
                return nullptr;
            }

        private:
            static optional< Value > ExecuteBuiltinFuncCall( const Value& func, const Term& args );
            static Term BuildUninitializedValue( const Value& type );

            template< typename F >
            Value executeEqualityBinOp( const llr::BinaryOp& bo, F&& func );

            template< typename F >
            Value executeLogicBinOp( const llr::BinaryOp& bo, F&& func );
︙︙
Changes to bs/sema/inv-ruleset.h.
︙︙
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

            virtual ~InvocationRule() {}

            virtual bool canBeInvoked( const Context& c, const Value& callee ) const
            {
                return true;
            }

            virtual Value resolveInvocation( const Context& c, uint32_t locationId, const Value& callee, const Value& args ) const = 0;

            virtual Value invoke( const Context& c, uint32_t locationId, const Value& callee, const Term& unifiedCallPat, UnificationContext& uc ) const
            {
                return PoisonValue();
            }

            virtual optional< Term > getSignature( const Value& callee ) const
            {
                return nullopt;








|

|








9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

            virtual ~InvocationRule() {}

            virtual bool canBeInvoked( const Context& c, const Value& callee ) const
            {
                return true;
            }

            virtual Value resolveInvocation( const Context& c, uint32_t locationId, const Value& callee, const Term& args ) const = 0;

            virtual Value invoke( const Context& c, uint32_t locationId, const Value& callee, const Term& args, const Term& unifiedCallPat, UnificationContext& uc ) const
            {
                return PoisonValue();
            }

            virtual optional< Term > getSignature( const Value& callee ) const
            {
                return nullopt;
︙︙
Changes to bs/sema/invocation.cpp.
︙︙
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62

        if( callee.isPoison() || args.isPoison() )
            return PoisonValue();

        auto loc = Location::CreateSpanningLocation( callee.locationId(), args.locationId() );
        if( loc == ~0 )
            DiagnosticsManager::GetInstance().setCurrentVerbosityLevel( Verbosity::Silent );

        auto result = pInvRule->resolveInvocation( c, loc, callee, args ).setLocationId( loc );

        // If the result is non-void, register it for destruction.
        // TODO probably just always store it as a numbered temporary
        // since we'll need this later to implement the dot operator
        // (as it will need to create a reference to the temporary)
        if( c.codeBuilder() && result.type() != GetValueType< void >() )
        {








|








48
49
50
51
52
53
54
55
56
57
58
59
60
61
62

        if( callee.isPoison() || args.isPoison() )
            return PoisonValue();

        auto loc = Location::CreateSpanningLocation( callee.locationId(), args.locationId() );
        if( loc == ~0 )
            DiagnosticsManager::GetInstance().setCurrentVerbosityLevel( Verbosity::Silent );

        auto result = pInvRule->resolveInvocation( c, loc, callee, args.val() ).setLocationId( loc );

        // If the result is non-void, register it for destruction.
        // TODO probably just always store it as a numbered temporary
        // since we'll need this later to implement the dot operator
        // (as it will need to create a reference to the temporary)
        if( c.codeBuilder() && result.type() != GetValueType< void >() )
        {
︙︙
Changes to bs/sema/overloadset.cpp.
︙︙
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

116
117
118
119
120
121
122


        return paramUTrie->merge( *params, uTrieMergeFunc );
    } );

    return success;
}

OverloadSet::UniGen OverloadSet::fullUnify( const Term& domPat, const Term& argsPat, const Term& rtPat, const Context& c ) const
{
    auto argDecomp = Decompose( argsPat,
        Val< pvec >()
    );

    if( !argDecomp )
        co_return;

    for( auto&& [domain,paramUTrie] : Enumerate( m_trie ) )
    {
        UnificationContext uc( c );
        uc.setComplexity( GetComplexity( domain ) + GetComplexity( domPat ) );

        for( auto&& [uniDom,uc] : Unify( domain, domPat, uc ) )
        {
            for( auto&& [paramsVec,uniParamsVec,rtTrie,uc] : paramUTrie->unify( *argDecomp->get(), uc ) )
            {
                auto params = TERM( make_shared< Vector >( paramsVec ) );
                auto uniParams = TERM( make_shared< Vector >( uniParamsVec ) );

                for( auto&& [rt,ovl] : Enumerate( rtTrie ) )
                {
                    auto localC = uc;
                    localC.addComplexity( GetComplexity( rt ) + GetComplexity( rtPat ) );

                    for( auto&& [uniRt,uc] : Unify( rt, rtPat, localC ) )
                    {
                        auto lhs = TERM( Vector::Make( domain, params, rt ) );
                        auto rhs = TERM( Vector::Make( domPat, argsPat, rtPat ) );
                        auto uniCall = TERM( Vector::Make( uniDom, uniParams, uniRt ) );

                        for( auto&& [s, uc] : UnifyPass2( lhs, rhs, uniCall, uc ) )
                            co_yield { s, ovl, uc };
                    }
                }
            }
        }
    }
}

OverloadSet::UniGen OverloadSet::unify( const Term& domPat, const Term& argsPat, const Term& rtPat, UnificationContext& uc ) const
{
    auto argDecomp = Decompose( argsPat,
        Val< pvec >()
    );

    if( !argDecomp )
        co_return;

    for( auto&& [domain,paramUTrie] : Enumerate( m_trie ) )
    {
        auto localC = uc;
        localC.addComplexity( GetComplexity( domain ) + GetComplexity( domPat ) );

        for( auto&& [uniDom,uc] : Unify( domain, domPat, localC ) )
        {
            for( auto&& [paramsVec,uniParamsVec,rtTrie,uc] : paramUTrie->unify( *argDecomp->get(), uc ) )
            {
                auto params = TERM( make_shared< Vector >( paramsVec ) );
                auto uniParams = TERM( make_shared< Vector >( uniParamsVec ) );

                for( auto&& [rt,ovl] : Enumerate( rtTrie ) )
                {
                    auto localC = uc;
                    localC.addComplexity( GetComplexity( rt ) + GetComplexity( rtPat ) );

                    for( auto&& [uniRt,uc] : Unify( rt, rtPat, localC ) )
                    {








<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
|



















>








48
49
50
51
52
53
54









































55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82


        return paramUTrie->merge( *params, uTrieMergeFunc );
    } );

    return success;
}










































OverloadSet::UniGen OverloadSet::unify( const Term& domPat, const Term& argsPat, const Term& rtPat, const UnificationContext& uc ) const
{
    auto argDecomp = Decompose( argsPat,
        Val< pvec >()
    );

    if( !argDecomp )
        co_return;

    for( auto&& [domain,paramUTrie] : Enumerate( m_trie ) )
    {
        auto localC = uc;
        localC.addComplexity( GetComplexity( domain ) + GetComplexity( domPat ) );

        for( auto&& [uniDom,uc] : Unify( domain, domPat, localC ) )
        {
            for( auto&& [paramsVec,uniParamsVec,rtTrie,uc] : paramUTrie->unify( *argDecomp->get(), uc ) )
            {
                auto params = TERM( make_shared< Vector >( paramsVec ) );
                auto uniParams = TERM( make_shared< Vector >( uniParamsVec ) );

                for( auto&& [rt,ovl] : Enumerate( rtTrie ) )
                {
                    auto localC = uc;
                    localC.addComplexity( GetComplexity( rt ) + GetComplexity( rtPat ) );

                    for( auto&& [uniRt,uc] : Unify( rt, rtPat, localC ) )
                    {
︙︙
Changes to bs/sema/overloadset.h.
︙︙
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38


            using UniGen = Generator< tuple<
                Term,
                const Overload&,
                UnificationContext
            > >;

            UniGen fullUnify( const Term& domPat, const Term& argsPat, const Term& rtPat, const Context& c ) const;
            UniGen unify( const Term& domPat, const Term& argsPat, const Term& rtPat, UnificationContext& uc ) const;

        private:
            Term m_identity;

            using trie_type = Trie< ptr< UTrie< Trie< Overload > > > >;
            trie_type m_trie;
    };








<
|








23
24
25
26
27
28
29

30
31
32
33
34
35
36
37


            using UniGen = Generator< tuple<
                Term,
                const Overload&,
                UnificationContext
            > >;


            UniGen unify( const Term& domPat, const Term& argsPat, const Term& rtPat, const UnificationContext& uc ) const;

        private:
            Term m_identity;

            using trie_type = Trie< ptr< UTrie< Trie< Overload > > > >;
            trie_type m_trie;
    };
︙︙
Changes to bs/sema/postprocess.cpp.
︙︙
31
32
33
34
35
36
37



























38
39
40
41
42
43
44


        auto&& [pPP, t] = *result;
        return make_pair( t, static_pointer_cast< PostProcFunc >( pPP ) );
    }

    optional< Term > Postprocess( const Term& src, UnificationContext& uc )
    {



























        if( !holds_alternative< pvec >( src ) )
            return src;

        if( auto optPP = UnwrapPostprocFunc( src ) )
        {
            auto val = Postprocess( optPP->first, uc );
            if( !val )








>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>








31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71


        auto&& [pPP, t] = *result;
        return make_pair( t, static_pointer_cast< PostProcFunc >( pPP ) );
    }

    optional< Term > Postprocess( const Term& src, UnificationContext& uc )
    {
        if( auto optHole = HoleFromIRExpr( src ) )
        {
            const auto& hole = *optHole;

            if( !hole.name.isNumerical() )
            {
                // If the name is not found, output it as is.
                auto index = uc.getLHSHoleIndex( hole.name );
                if( index == UnificationContext::InvalidIndex )
                    return src;

                const auto& val = uc.getValue( index );
                if( !val )
                    return src;

                return Postprocess( *val, uc );
            }
            else
            {
                const auto& optVal = uc.getValue( hole.name.id() );
                if( !optVal )
                    return HOLE( "_"_sid );

                return Postprocess( *optVal, uc );
            }
        }

        if( !holds_alternative< pvec >( src ) )
            return src;

        if( auto optPP = UnwrapPostprocFunc( src ) )
        {
            auto val = Postprocess( optPP->first, uc );
            if( !val )
︙︙
Changes to bs/sema/substitute.cpp.
︙︙
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79


        auto outputTerms = make_shared< Vector >();
        outputTerms->reserve( vec.terms().size() );

        for( auto&& t : vec.terms() )
            outputTerms->append( Substitute( t, context ) );

        return outputTerms;
    }

    Term SubstituteNamed( const Term& src, const UnificationContext& context )
    {
        if( auto optHole = HoleFromIRExpr( src ) )
        {
            const auto& hole = *optHole;

            if( !hole.name.isNumerical() )
            {
                // If the name is not found, output it as is.
                auto index = context.getLHSHoleIndex( hole.name );
                if( index == UnificationContext::InvalidIndex )
                    return src;

                const auto& val = context.getValue( index );
                if( !val )
                    return src;

                return SubstituteNamed( *val, context );
            }
            else
            {
                const auto& optVal = context.getValue( hole.name.id() );
                if( !optVal )
                    return HOLE( "_"_sid );

                return SubstituteNamed( *optVal, context );
            }
        }

        if( !holds_alternative< pvec >( src ) )
            return src;

        const auto& vec = *get< pvec >( src );

        auto outputTerms = make_shared< Vector >();
        outputTerms->reserve( vec.terms().size() );

        for( auto&& t : vec.terms() )
            outputTerms->append( SubstituteNamed( t, context ) );

        return outputTerms;
    }
}








<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<




27
28
29
30
31
32
33











































34
35
36


        auto outputTerms = make_shared< Vector >();
        outputTerms->reserve( vec.terms().size() );

        for( auto&& t : vec.terms() )
            outputTerms->append( Substitute( t, context ) );












































        return outputTerms;
    }
}
Changes to bs/sema/substitute.h. 
1
2
3
4
5
6
7
8
9
10

#ifndef GOOSE_SEMA_SUBSTITUTE_H
#define GOOSE_SEMA_SUBSTITUTE_H

namespace goose::sema
{
    extern Term Substitute( const Term& src, const UnificationContext& context );
    extern Term SubstituteNamed( const Term& src, const UnificationContext& context );
}

#endif







<




1
2
3
4
5
6

7
8
9

#ifndef GOOSE_SEMA_SUBSTITUTE_H
#define GOOSE_SEMA_SUBSTITUTE_H

namespace goose::sema
{
    extern Term Substitute( const Term& src, const UnificationContext& context );

}

#endif
Changes to bs/sema/tests/unify-holes.cpp.
︙︙
12
13
14
15
16
17
18


19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39


40
41
42
43
44
45
46
47
48

namespace
{
    // Verifies that the unification of lhs and rhs yields only one solution, that it is complete,
    // and that this solution is the expected one.
    void CheckForUniqueSolution( const Term& lhs, const Term& rhs, const Term& expectedSolution, const UnificationScore& expectedScore )
    {
        Context ctxt( make_shared< Env >(), VEC( TSID( g0 ) ) );



        auto g = FullUnify( lhs, rhs, ctxt );

        auto it = g.begin();
        REQUIRE( it != g.end() );

        auto&& [e,c] = *it;

        REQUIRE( c.numUnknownValues() == 0 );
        REQUIRE( c.score() == expectedScore );

        auto sol = Substitute( e, c );
        REQUIRE( sol == expectedSolution );

        ++it;
        REQUIRE( it == g.end() );
    }

    void CheckForNoSolution( const Term& lhs, const Term& rhs )
    {
        Context ctxt( make_shared< Env >(), VEC( TSID( g0 ) ) );



        auto g = FullUnify( lhs, rhs, ctxt );

        auto it = g.begin();
        REQUIRE( it == g.end() );
    }
}

SCENARIO( "Unify works", "[unify]" )








>
>

|









|









>
>

|








12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

namespace
{
    // Verifies that the unification of lhs and rhs yields only one solution, that it is complete,
    // and that this solution is the expected one.
    void CheckForUniqueSolution( const Term& lhs, const Term& rhs, const Term& expectedSolution, const UnificationScore& expectedScore )
    {
        Context ctxt( make_shared< Env >(), VEC( TSID( g0 ) ) );
        UnificationContext uc( ctxt );
        uc.setComplexity( GetComplexity( lhs ) + GetComplexity( rhs ) );

        auto g = Unify( lhs, rhs, uc );

        auto it = g.begin();
        REQUIRE( it != g.end() );

        auto&& [e,c] = *it;

        REQUIRE( c.numUnknownValues() == 0 );
        REQUIRE( c.score() == expectedScore );

        auto sol = Postprocess( e, c );
        REQUIRE( sol == expectedSolution );

        ++it;
        REQUIRE( it == g.end() );
    }

    void CheckForNoSolution( const Term& lhs, const Term& rhs )
    {
        Context ctxt( make_shared< Env >(), VEC( TSID( g0 ) ) );
        UnificationContext uc( ctxt );
        uc.setComplexity( GetComplexity( lhs ) + GetComplexity( rhs ) );

        auto g = Unify( lhs, rhs, uc );

        auto it = g.begin();
        REQUIRE( it == g.end() );
    }
}

SCENARIO( "Unify works", "[unify]" )
︙︙
Changes to bs/sema/tests/utrie-unify.cpp.
︙︙
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

        vector< tuple< Term, string, UnificationScore > > solutions;

        for( auto&& [lv, v,content,c] : trie->unify( vec, context ) )
        {
            if( c.numUnknownValues() )
                continue;

            auto sol = Substitute( TERM( make_shared< Vector >( v ) ), c );
            solutions.emplace_back( sol, content, c.score() );
        }

        sort( solutions.begin(), solutions.end(), []( auto&& a, auto&& b )
        {
            return get< 1 >( a ) < get< 1 >( b );
        } );









|
|








19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

        vector< tuple< Term, string, UnificationScore > > solutions;

        for( auto&& [lv, v,content,c] : trie->unify( vec, context ) )
        {
            if( c.numUnknownValues() )
                continue;

            auto sol = Postprocess( TERM( make_shared< Vector >( v ) ), c );
            solutions.emplace_back( *sol, content, c.score() );
        }

        sort( solutions.begin(), solutions.end(), []( auto&& a, auto&& b )
        {
            return get< 1 >( a ) < get< 1 >( b );
        } );
︙︙
Changes to bs/sema/uni-context.h.
︙︙
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63

            }

            bool isValueResolutionRequired() const
            {
                return m_valuesAreRequired;
            }

            // Indicates whether we are in trhe second unification pass
            bool secondPass() const { return m_secondPass; }

            void setSecondPass() { m_secondPass = true; }

            const optional< Term >& getValue( uint32_t index ) const
            {
                assert( m_pCow->values.size() > index );
                return m_pCow->values[index].m_term;
            }

            template< typename T >








<
<
<
<
<








45
46
47
48
49
50
51





52
53
54
55
56
57
58

            }

            bool isValueResolutionRequired() const
            {
                return m_valuesAreRequired;
            }






            const optional< Term >& getValue( uint32_t index ) const
            {
                assert( m_pCow->values.size() > index );
                return m_pCow->values[index].m_term;
            }

            template< typename T >
︙︙
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108

            void subComplexity( uint32_t c ) { m_complexity -=c; }
            void setComplexity( uint32_t complexity ) { m_complexity = complexity; }

            void addAnonymousHole() { ++m_numAnonymousHoles; }

            auto score() const { return UnificationScore( m_complexity, m_pCow->holeDict.size() + m_numAnonymousHoles ); }

            bool substitutionNeeded() const
            {
                return m_pCow->holeDict.size() > 0
                    || m_numAnonymousHoles > 0;
            }

            // Used to detect and reject recursive hole nesting.
            bool isHoleLocked( uint32_t index ) const;
            void lockHole( uint32_t index );
            void unlockHole( uint32_t index );

        private:
            void setValueRequired( uint32_t index );








<
<
<
<
<
<








84
85
86
87
88
89
90






91
92
93
94
95
96
97

            void subComplexity( uint32_t c ) { m_complexity -=c; }
            void setComplexity( uint32_t complexity ) { m_complexity = complexity; }

            void addAnonymousHole() { ++m_numAnonymousHoles; }

            auto score() const { return UnificationScore( m_complexity, m_pCow->holeDict.size() + m_numAnonymousHoles ); }







            // Used to detect and reject recursive hole nesting.
            bool isHoleLocked( uint32_t index ) const;
            void lockHole( uint32_t index );
            void unlockHole( uint32_t index );

        private:
            void setValueRequired( uint32_t index );
︙︙
132
133
134
135
136
137
138
139
140
141
142
143

                unordered_map< HoleName, uint32_t > holeDict;
                unordered_set< uint32_t >           lockedHoles;
            };

            ptr< Cow >                                  m_pCow = make_shared< Cow >();

            bool                                        m_valuesAreRequired = true;
            bool                                        m_secondPass = false;
    };
}

#endif








<





121
122
123
124
125
126
127

128
129
130
131

                unordered_map< HoleName, uint32_t > holeDict;
                unordered_set< uint32_t >           lockedHoles;
            };

            ptr< Cow >                                  m_pCow = make_shared< Cow >();

            bool                                        m_valuesAreRequired = true;

    };
}

#endif
Changes to bs/sema/unify.cpp. 
1
2
3
4
5
6
7
8
9
10



11
12



13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

#include "sema.h"

namespace goose::sema
{
    UnificationSolution FindBestUnification( const Term& lhs, const Term& rhs, const Context& context )
    {
        optional< UnificationContext > bestUC;
        optional< Term > bestSol;
        bool ambiguous = false;




        for( auto&& [s, uc] : FullUnify( lhs, rhs, context ) )
        {



            if( bestSol && uc.score() < bestUC->score() )
                continue;

            auto pps = Postprocess( s, uc );
            if( !pps )
                continue;

            if( uc.score() == bestUC->score() )
            {
                ambiguous = true;
                continue;
            }

            bestUC = uc;
            bestSol = move( *pps );
            ambiguous = false;
        }

        if( !bestSol )
            return {};

        if( ambiguous )
            return AmbiguousUnification{};

        return make_pair( move( *bestSol ), move( *bestUC ) );
    }

    UniGen FullUnify( const Term& lhs, const Term& rhs, const Context& context )
    {
        UnificationContext uc( context );
        uc.setComplexity( GetComplexity( lhs ) + GetComplexity( rhs ) );

        for( auto&& [s, ucPass1] : Unify( lhs, rhs, uc ) )
        {
            for( auto&& [s, uc] : UnifyPass2( lhs, rhs, s, ucPass1 ) )
                co_yield { s, uc };
        }
    }

    // If substitution is needed, perform substitution on lhs and rhs and then
    // perform a second unification pass.
    UniGen UnifyPass2( const Term& lhs, const Term& rhs, const Term& s, UnificationContext ucPass1 )
    {
        if( ucPass1.numUnknownValues() )
            co_return;

        auto slhs = SubstituteNamed( lhs, ucPass1 );
        auto srhs = SubstituteNamed( rhs, ucPass1.flip() );

        ucPass1.setSecondPass();
        for( auto&& [s, ucPass2] : Unify( slhs, srhs, ucPass1.flip() ) )
        {
            ucPass2.setComplexity( ucPass1.complexity() );
            co_yield { Substitute( s, ucPass2 ), ucPass2 };
        }
    }

    UniGen Unify( const Term& lhs, const Term& rhs, const UnificationContext& context )
    {
        const auto& rules = context.rules()->uniRules();

        MatchSolution bestSol;











>
>
>
|

>
>
>
|






|










<
<
<



<
<
|
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
<
|

<
<
|
<
<
<
<
<
<








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36



37
38
39


40

















41
42


43






44
45
46
47
48
49
50

#include "sema.h"

namespace goose::sema
{
    UnificationSolution FindBestUnification( const Term& lhs, const Term& rhs, const Context& context )
    {
        optional< UnificationContext > bestUC;
        optional< Term > bestSol;
        bool ambiguous = false;

        UnificationContext uc( context );
        uc.setComplexity( GetComplexity( lhs ) + GetComplexity( rhs ) );

        for( auto&& [s, uc] : Unify( lhs, rhs, uc ) )
        {
            if( uc.numUnknownValues() )
                continue;

            if( bestUC && uc.score() < bestUC->score() )
                continue;

            auto pps = Postprocess( s, uc );
            if( !pps )
                continue;

            if( bestUC && uc.score() == bestUC->score() )
            {
                ambiguous = true;
                continue;
            }

            bestUC = uc;
            bestSol = move( *pps );
            ambiguous = false;
        }




        if( ambiguous )
            return AmbiguousUnification{};



        if( !bestSol )

















            return {};



        return make_pair( move( *bestSol ), move( *bestUC ) );






    }

    UniGen Unify( const Term& lhs, const Term& rhs, const UnificationContext& context )
    {
        const auto& rules = context.rules()->uniRules();

        MatchSolution bestSol;
︙︙
Changes to bs/sema/unify.h.
︙︙
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

        UniSol
    >;

    UnificationSolution FindBestUnification( const Term& lhs, const Term& rhs, const Context& context );

    using UniGen = Generator< pair< Term, UnificationContext > >;

    // Perform one unification pass, or two if holes need to be substituted.
    UniGen FullUnify( const Term& lhs, const Term& rhs, const Context& context );

    // If substitution is needed, perform substitution on lhs and rhs and then
    // perform a second unification pass.
    UniGen UnifyPass2( const Term& lhs, const Term& rhs, const Term& s, UnificationContext ucPass1 );

    // Perform one unification pass
    UniGen Unify( const Term& lhs, const Term& rhs, const UnificationContext& context );

    UniGen HalfUnify( const Term& lhs, const UnificationContext& context );
}

#endif








<
<
<
<
<
<
<
<

<





14
15
16
17
18
19
20








21

22
23
24
25

        UniSol
    >;

    UnificationSolution FindBestUnification( const Term& lhs, const Term& rhs, const Context& context );

    using UniGen = Generator< pair< Term, UnificationContext > >;









    UniGen Unify( const Term& lhs, const Term& rhs, const UnificationContext& context );

    UniGen HalfUnify( const Term& lhs, const UnificationContext& context );
}

#endif
Changes to bs/verify/builder.cpp.
︙︙
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116

    if( m_remapper )
    {
        m_remapper->forEachIncomingEdge( bbIndex, [&]( auto&& predIndex, auto&& expr )
        {
            if( auto predVar = retrieveVar( index, predIndex ) )
            {
                if( !newVar )
                    newVar = BuildZ3ConstantFromType( context(), predVar->type, format( "v{}", m_nextUniqueId++ ) );

                if( newVar->expr.is_int() )
                {
                    add( z3::implies( c.bool_const( format( "e{}_{}", predIndex, bbIndex ).c_str() ),
                        newVar->expr == GetAsInt( predVar->expr, newVar->type ) ) );
                }
                else if( newVar->expr.is_bv() )








|








102
103
104
105
106
107
108
109
110
111
112
113
114
115
116

    if( m_remapper )
    {
        m_remapper->forEachIncomingEdge( bbIndex, [&]( auto&& predIndex, auto&& expr )
        {
            if( auto predVar = retrieveVar( index, predIndex ) )
            {
                if( !newVar )
                    newVar = BuildZ3ConstantFromType( *this, predVar->type, format( "v{}", m_nextUniqueId++ ) );

                if( newVar->expr.is_int() )
                {
                    add( z3::implies( c.bool_const( format( "e{}_{}", predIndex, bbIndex ).c_str() ),
                        newVar->expr == GetAsInt( predVar->expr, newVar->type ) ) );
                }
                else if( newVar->expr.is_bv() )
︙︙
Changes to bs/verify/builder.h.
︙︙
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

        public:
            Builder( const sema::Context& c, z3::solver& solver, Remapper* remapper = nullptr ) :
                m_context( &c ),
                m_solver( &solver ),
                m_remapper( remapper )
            {}

            const auto& context() { return *m_context; }
            auto* solver() { return m_solver; }
            auto* remapper() { return m_remapper; }
            uint32_t currentBBIndex() const { return m_currentBBIndex; }

            void setTraceMode( bool b ) { m_traceMode = b; }

            void setCFG( const ptr< llr::CFG >& cfg )








|








19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

        public:
            Builder( const sema::Context& c, z3::solver& solver, Remapper* remapper = nullptr ) :
                m_context( &c ),
                m_solver( &solver ),
                m_remapper( remapper )
            {}

            const auto& context() const { return *m_context; }
            auto* solver() { return m_solver; }
            auto* remapper() { return m_remapper; }
            uint32_t currentBBIndex() const { return m_currentBBIndex; }

            void setTraceMode( bool b ) { m_traceMode = b; }

            void setCFG( const ptr< llr::CFG >& cfg )
︙︙
Changes to bs/verify/call.cpp.
︙︙
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

            return nullopt;

        const auto& ft = func->type();
        const auto& fvi = ft.verifInfos();
        if( !fvi )
            return nullopt;

        auto retExpr = BuildZ3ConstantFromType( b.context(), ft.returnType(), format( "r{}", b.newUniqueId() ) );

        // Create a temporary builder to construct the z3 expressions out of the
        // function's pre-conditions and postconditions, configured
        // to perform the necessary replacements for arguments and for the
        // return value placeholder.
        Builder cb( b.context(), *b.solver(), b.remapper() );









|








13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

            return nullopt;

        const auto& ft = func->type();
        const auto& fvi = ft.verifInfos();
        if( !fvi )
            return nullopt;

        auto retExpr = BuildZ3ConstantFromType( b, ft.returnType(), format( "r{}", b.newUniqueId() ) );

        // Create a temporary builder to construct the z3 expressions out of the
        // function's pre-conditions and postconditions, configured
        // to perform the necessary replacements for arguments and for the
        // return value placeholder.
        Builder cb( b.context(), *b.solver(), b.remapper() );
︙︙
Changes to bs/verify/condition.cpp.
︙︙
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

        );

        if( !result )
            return true;

        auto&& [type, val, locId] = *result;

        if( auto paramInit = BuildZ3ConstantFromType( c, type, format( "p{}", varId ) ) )
            m_builder.setVar( varId, move( *paramInit ) );

        ++varId;
        return true;
    } );
}









|








33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

        );

        if( !result )
            return true;

        auto&& [type, val, locId] = *result;

        if( auto paramInit = BuildZ3ConstantFromType( m_builder, type, format( "p{}", varId ) ) )
            m_builder.setVar( varId, move( *paramInit ) );

        ++varId;
        return true;
    } );
}
︙︙
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104

                "invalid condition." );
            return true;
        }

        stringstream sstr;
        sstr << '$' << m_nextIndex++;

        auto boolCst = GetZ3Context().bool_const(sstr.str().c_str());
        m_idAndLocs.emplace_back( boolCst.id(), val.locationId() );

        m_solver.add( zv->expr, boolCst );
        return true;
    } );

    return success;
}

bool Condition::verify()
{
    if( m_solver.check() == z3::check_result::sat )
        return true;

    // TODO: emit a general "those verification expressions fucking suck"
    // if it's neither sat or unsat.

    // Retrieve the unsat core to find out which assertions are unsatisfiable,
    // and emit error messages.
    auto unsatCore = m_solver.unsat_core();

    llvm::SmallVector< uint32_t, 8 > errorLocations;









|














|
|








74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104

                "invalid condition." );
            return true;
        }

        stringstream sstr;
        sstr << '$' << m_nextIndex++;

        auto boolCst = GetZ3Context().bool_const( sstr.str().c_str() );
        m_idAndLocs.emplace_back( boolCst.id(), val.locationId() );

        m_solver.add( zv->expr, boolCst );
        return true;
    } );

    return success;
}

bool Condition::verify()
{
    if( m_solver.check() == z3::check_result::sat )
        return true;

    // TODO: emit a generic "those verification expressions fucking suck"
    // error if it's neither sat or unsat.

    // Retrieve the unsat core to find out which assertions are unsatisfiable,
    // and emit error messages.
    auto unsatCore = m_solver.unsat_core();

    llvm::SmallVector< uint32_t, 8 > errorLocations;
︙︙
Changes to bs/verify/func.cpp.
︙︙
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84

                    if( !result )
                        return true;

                    auto&& [type, val, locId] = *result;
                    auto paramVal = BuildComputedValue( type, llr::Load( llr::VarAddress( varId ), type ) );

                    // Initialize every parameter containing variable with an freshly named constant of the right type.
                    if( auto paramInit = BuildZ3ConstantFromType( m_builder.context(), type, format( "p{}", varId ) ) )
                        m_builder.setVar( varId, move( *paramInit ) );

                    ++varId;

                    if( auto zv = BuildZ3ExprFromValue( m_builder, paramVal ) )
                    {
                        ForEachPredicate( m_builder, type, zv->expr, [&]( auto&& z3expr, auto locId )








|








70
71
72
73
74
75
76
77
78
79
80
81
82
83
84

                    if( !result )
                        return true;

                    auto&& [type, val, locId] = *result;
                    auto paramVal = BuildComputedValue( type, llr::Load( llr::VarAddress( varId ), type ) );

                    // Initialize every parameter containing variable with an freshly named constant of the right type.
                    if( auto paramInit = BuildZ3ConstantFromType( m_builder, type, format( "p{}", varId ) ) )
                        m_builder.setVar( varId, move( *paramInit ) );

                    ++varId;

                    if( auto zv = BuildZ3ExprFromValue( m_builder, paramVal ) )
                    {
                        ForEachPredicate( m_builder, type, zv->expr, [&]( auto&& z3expr, auto locId )
︙︙
Changes to bs/verify/phi.cpp. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

#include "verify.h"
#include "builtins/builtins.h"

namespace goose::verify
{
    optional< Z3Val > BuildZ3Op( Builder& b, const Phi& instr )
    {
        const auto* remapper = b.remapper();
        if( !remapper )
            return nullopt;

        auto newVar = BuildZ3ConstantFromType( b.context(), instr.type(), format( "v{}", b.newUniqueId() ) );
        if( !newVar )
            return nullopt;

        auto& c = GetZ3Context();
        uint32_t bbIndex = b.currentBBIndex();

        // Model the ssa phi operation by creating a series of equality assertions, each implied by












|








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

#include "verify.h"
#include "builtins/builtins.h"

namespace goose::verify
{
    optional< Z3Val > BuildZ3Op( Builder& b, const Phi& instr )
    {
        const auto* remapper = b.remapper();
        if( !remapper )
            return nullopt;

        auto newVar = BuildZ3ConstantFromType( b, instr.type(), format( "v{}", b.newUniqueId() ) );
        if( !newVar )
            return nullopt;

        auto& c = GetZ3Context();
        uint32_t bbIndex = b.currentBBIndex();

        // Model the ssa phi operation by creating a series of equality assertions, each implied by
︙︙
Changes to bs/verify/storage.cpp.
︙︙
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

            if( !tinfo )
                return nullopt;

            // The only aggregate type that we handle for now are tuples.
            // TODO: arrays
            auto elemType = GetTupleTypeElement( val->type, index );
            auto elemExpr = tinfo->proj( val->expr, index );
            if( !elemExpr )
                return nullopt;

            val = Z3Val{ *elemExpr, *ValueFromIRExpr( elemType ) };
        }

        return val;
    }

    optional< Z3Val > LoadFromAddress( Builder& b, const BaseAddress& baseAddr )
    {








<
<
<
|








18
19
20
21
22
23
24



25
26
27
28
29
30
31
32

            if( !tinfo )
                return nullopt;

            // The only aggregate type that we handle for now are tuples.
            // TODO: arrays
            auto elemType = GetTupleTypeElement( val->type, index );
            auto elemExpr = tinfo->proj( val->expr, index );



            val = Z3Val{ move( elemExpr ), *ValueFromIRExpr( elemType ) };
        }

        return val;
    }

    optional< Z3Val > LoadFromAddress( Builder& b, const BaseAddress& baseAddr )
    {
︙︙
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107


        auto elemIndex = path[index];

        for( uint32_t i = 0; i < elemCount; ++i )
        {
            auto elemType = GetTupleTypeElement( aggregate.type, i );
            auto elemExpr = tinfo->proj( aggregate.expr, i );
            if( !elemExpr )
                return nullopt;

            // Copy all elements from the existing value as is,
            // except for the one pointed to by the current path index.
            if( i == elemIndex )
            {
                // If we didn't reach the end of the path yet, recurse.
                // Otherwise, it means we finally reached the nested member that we wanted to modify,
                // so push the new value.
                if( index < ( path.size() - 1 ) )
                {
                    auto newElem = ModifyAggregate( b, Z3Val{ *elemExpr, *ValueFromIRExpr( elemType ) }, path, ++index, move( valToStore ) );
                    if( !newElem )
                        return nullopt;

                    args.push_back( *newElem );
                }
                else
                    args.push_back( valToStore.expr );
            }
            else
            {
                assert( elemExpr );
                args.push_back( *elemExpr );
            }
        }

        return tinfo->ctor( args );
    }

    void StoreToAddress( Builder& b, const Address& addr, Z3Val&& valToStore )
    {








<
<










|



|





<
<
|
<








65
66
67
68
69
70
71


72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91


92

93
94
95
96
97
98
99


        auto elemIndex = path[index];

        for( uint32_t i = 0; i < elemCount; ++i )
        {
            auto elemType = GetTupleTypeElement( aggregate.type, i );
            auto elemExpr = tinfo->proj( aggregate.expr, i );



            // Copy all elements from the existing value as is,
            // except for the one pointed to by the current path index.
            if( i == elemIndex )
            {
                // If we didn't reach the end of the path yet, recurse.
                // Otherwise, it means we finally reached the nested member that we wanted to modify,
                // so push the new value.
                if( index < ( path.size() - 1 ) )
                {
                    auto newElem = ModifyAggregate( b, Z3Val{ move( elemExpr ), *ValueFromIRExpr( elemType ) }, path, ++index, move( valToStore ) );
                    if( !newElem )
                        return nullopt;

                    args.push_back( move( *newElem ) );
                }
                else
                    args.push_back( valToStore.expr );
            }
            else


                args.push_back( move( elemExpr ) );

        }

        return tinfo->ctor( args );
    }

    void StoreToAddress( Builder& b, const Address& addr, Z3Val&& valToStore )
    {
︙︙
177
178
179
180
181
182
183
184
185
186
187
188
189
190

    void StoreToAddressForBB( Builder& b, uint32_t bbIndex, const llr::VarAddress& va, Z3Val&& val )
    {
        b.setVarForBasicBlock( bbIndex, va.index, move( val ) );
    }

    void HavocAddressForBB( Builder& b, uint32_t bbIndex, const Term& type, const Address& addr )
    {
        auto valToStore = BuildZ3ConstantFromType( b.context(), type, format( "v{}", b.newUniqueId() ) );
        if( !valToStore )
            return;

        StoreToAddressForBB( b, bbIndex, addr, move( *valToStore ) );
    }
}








|







169
170
171
172
173
174
175
176
177
178
179
180
181
182

    void StoreToAddressForBB( Builder& b, uint32_t bbIndex, const llr::VarAddress& va, Z3Val&& val )
    {
        b.setVarForBasicBlock( bbIndex, va.index, move( val ) );
    }

    void HavocAddressForBB( Builder& b, uint32_t bbIndex, const Term& type, const Address& addr )
    {
        auto valToStore = BuildZ3ConstantFromType( b, type, format( "v{}", b.newUniqueId() ) );
        if( !valToStore )
            return;

        StoreToAddressForBB( b, bbIndex, addr, move( *valToStore ) );
    }
}
Changes to bs/verify/type.cpp.
︙︙
45
46
47
48
49
50
51
52




53
54
55
56
57
58
59
60
61
62
63
64




65
66
67
68
69
70
71
72
73

74
75




76
77
78
79
80
81
82

optional< TypeInfo > TypeCache::CreateTypeInfoForBasicType( const sema::Context& c, const Value& typeVal )
{
    // Handle all non-aggregate types (bool, signed int, unsigned int, floats) directly.
    // TODO: some are missing and will be dealt with later on.
    if( ValueToIRExpr( typeVal ) == GetValueType< bool >() )
    {
        return TypeInfo { GetZ3Context().bool_sort(),
            []( auto&& c, auto&& val )




            {
                return GetZ3Context().bool_val( *FromValue< bool >( val ) );
            }
        };
    }

    if( auto intType = FromValue< builtins::IntegerType >( typeVal ) )
    {
        if( intType->m_signed )
        {
            return TypeInfo { GetZ3Context().int_sort(),
                []( auto&& c, auto&& val )




                {
                    auto intVal = FromValue< APSInt >( val );
                    return GetZ3Context().int_val( intVal->getExtValue() );
                }
            };
        }
        else
        {
            auto numBits = intType->m_numBits;

            return TypeInfo { GetZ3Context().bv_sort( intType->m_numBits ),
                [numBits]( auto&& c, auto&& val )




                {
                    auto intVal = FromValue< APSInt >( val );
                    return GetZ3Context().bv_val( intVal->getExtValue(), numBits );
                }
            };
        }
    }








|
>
>
>
>











|
>
>
>
>









>

|
>
>
>
>








45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95

optional< TypeInfo > TypeCache::CreateTypeInfoForBasicType( const sema::Context& c, const Value& typeVal )
{
    // Handle all non-aggregate types (bool, signed int, unsigned int, floats) directly.
    // TODO: some are missing and will be dealt with later on.
    if( ValueToIRExpr( typeVal ) == GetValueType< bool >() )
    {
        return TypeInfo { GetZ3Context().bool_sort(),
            []( auto&& b )
            {
                return GetZ3Context().bool_const( format( "u{}", b.newUniqueId() ).c_str() );
            },
            []( auto&& b, auto&& val )
            {
                return GetZ3Context().bool_val( *FromValue< bool >( val ) );
            }
        };
    }

    if( auto intType = FromValue< builtins::IntegerType >( typeVal ) )
    {
        if( intType->m_signed )
        {
            return TypeInfo { GetZ3Context().int_sort(),
                []( auto&& b )
                {
                    return GetZ3Context().int_const( format( "u{}", b.newUniqueId() ).c_str() );
                },
                []( auto&& b, auto&& val )
                {
                    auto intVal = FromValue< APSInt >( val );
                    return GetZ3Context().int_val( intVal->getExtValue() );
                }
            };
        }
        else
        {
            auto numBits = intType->m_numBits;

            return TypeInfo { GetZ3Context().bv_sort( intType->m_numBits ),
                [numBits]( auto&& b )
                {
                    return GetZ3Context().bv_const( format( "u{}", b.newUniqueId() ).c_str(), numBits );
                },
                [numBits]( auto&& b, auto&& val )
                {
                    auto intVal = FromValue< APSInt >( val );
                    return GetZ3Context().bv_val( intVal->getExtValue(), numBits );
                }
            };
        }
    }
︙︙
126
127
128
129
130
131
132














133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170

        elemSorts.push_back( *tinfo->sort );
    }

    llvm::SmallVector< z3::func_decl, 8 > projs;
    auto&& [tupSort, tupCtor] = mkZ3TupleSort( sortName.c_str(), size, elemNames, elemSorts, projs );
    const auto& ctor = tupCtor;















    auto build = [size, elemTInfos, ctor]( auto&& c, auto&& val )
    {
        llvm::SmallVector< z3::expr, 8 > args;
        args.reserve( size );

        uint32_t i = 0;
        bool success = true;

        ForEachInTuple( val, [&]( auto&& elemVal )
        {
            auto elem = BuildZ3ValFromConstant( c, elemVal );

            if( !elem )
            {
                success = false;
                return false;
            }

            args.push_back( elem->expr );
            return true;
        } );

        return ctor( args.size(), &args.front() );
    };

    auto proj = [projs]( auto&& tup, auto&& index )
    {
        assert( index < projs.size() );
        return projs[index]( tup );
    };

    auto ctorWrapper = [ctor]( auto&& args )
    {
        return ctor( args.size(), &args.front() );
    };

    return TypeInfo { tupSort, build, proj, ctorWrapper };
}








>
>
>
>
>
>
>
>
>
>
>
>
>
>
|





<
<


<
|
<
<
<
<
<
<
|

















|


139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165


166
167

168






169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188

        elemSorts.push_back( *tinfo->sort );
    }

    llvm::SmallVector< z3::func_decl, 8 > projs;
    auto&& [tupSort, tupCtor] = mkZ3TupleSort( sortName.c_str(), size, elemNames, elemSorts, projs );
    const auto& ctor = tupCtor;

    auto undefined = [size, elemTInfos, ctor]( auto&& b )
    {
        llvm::SmallVector< z3::expr, 8 > args;
        args.reserve( size );

        for( auto&& tinfo : elemTInfos )
        {
            auto elem = tinfo.undefined( b );
            args.push_back( move( elem ) );
        }

        return ctor( args.size(), &args.front() );
    };

    auto build = [size, elemTInfos, ctor]( auto&& b, auto&& val )
    {
        llvm::SmallVector< z3::expr, 8 > args;
        args.reserve( size );

        uint32_t i = 0;


        ForEachInTuple( val, [&]( auto&& elemVal )
        {

            auto elem = elemTInfos[i++].build( b, elemVal );






            args.push_back( move( elem ) );
            return true;
        } );

        return ctor( args.size(), &args.front() );
    };

    auto proj = [projs]( auto&& tup, auto&& index )
    {
        assert( index < projs.size() );
        return projs[index]( tup );
    };

    auto ctorWrapper = [ctor]( auto&& args )
    {
        return ctor( args.size(), &args.front() );
    };

    return TypeInfo { tupSort, undefined, build, proj, ctorWrapper };
}
Changes to bs/verify/type.h. 
1
2
3
4
5
6
7
8

9
10
11
12
13
14
15
16
17
18

#ifndef GOOSE_VERIFY_TYPE_H
#define GOOSE_VERIFY_TYPE_H

namespace goose::verify
{
    struct TypeInfo
    {
        optional< z3::sort > sort;

        function< optional< z3::expr >( const sema::Context&, const Value& ) > build;
        function< optional< z3::expr >( const z3::expr&, uint32_t index ) > proj;
        function< z3::expr( llvm::SmallVector< z3::expr, 8 > ) > ctor;
    };

    // For complex types that require the creation of custom constructor funcs in z3
    // (for instances tuples), we keep a cache to avoid recreating them multiple times.
    class TypeCache
    {
        public:









>
|
|
|








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

#ifndef GOOSE_VERIFY_TYPE_H
#define GOOSE_VERIFY_TYPE_H

namespace goose::verify
{
    struct TypeInfo
    {
        optional< z3::sort > sort;
        function< z3::expr ( Builder& ) > undefined;
        function< z3::expr ( Builder&, const Value& ) > build;
        function< z3::expr ( const z3::expr&, uint32_t index ) > proj;
        function< z3::expr ( llvm::SmallVector< z3::expr, 8 > ) > ctor;
    };

    // For complex types that require the creation of custom constructor funcs in z3
    // (for instances tuples), we keep a cache to avoid recreating them multiple times.
    class TypeCache
    {
        public:
︙︙
Changes to bs/verify/value.cpp. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

#include "verify.h"
#include "builtins/builtins.h"
#include "helpers.inl"

using namespace goose::diagnostics;

namespace goose::verify
{
    optional< Z3Val > BuildZ3ValFromConstant( const sema::Context& c, const Value& val )
    {
        auto loweredVal = LowerConstantForVerification( c, val );
        if( !loweredVal || loweredVal->isPoison() )
            return nullopt;

        auto tinfo = TypeCache::GetInstance()->getTypeInfo( c, loweredVal->type() );
        if( !tinfo )
            return nullopt;

        auto zexpr = tinfo->build( c, *loweredVal );
        if( !zexpr )
            return nullopt;

        return Z3Val { *zexpr, *ValueFromIRExpr( val.type() ) };
    }

    optional< Z3Val > BuildZ3ConstantFromType( const sema::Context& c, const Value& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance()->getTypeInfo( c, ValueToIRExpr( type ) );
        if( !tinfo )
            return nullopt;

        assert( tinfo->sort );
        return Z3Val { GetZ3Context().constant( name.c_str(), *tinfo->sort ), type };
    }

    optional< Z3Val > BuildZ3ConstantFromType( const sema::Context& c, const Term& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance()->getTypeInfo( c, type );
        if( !tinfo )
            return nullopt;

        assert( tinfo->sort );
        return Z3Val { GetZ3Context().constant( name.c_str(), *tinfo->sort ), *ValueFromIRExpr( type ) };
    }










|

|



|



|
<
<
<
|


|

|







|

|








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19



20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

#include "verify.h"
#include "builtins/builtins.h"
#include "helpers.inl"

using namespace goose::diagnostics;

namespace goose::verify
{
    optional< Z3Val > BuildZ3ValFromConstant( Builder& b, const Value& val )
    {
        auto loweredVal = LowerConstantForVerification( b.context(), val );
        if( !loweredVal || loweredVal->isPoison() )
            return nullopt;

        auto tinfo = TypeCache::GetInstance()->getTypeInfo( b.context(), loweredVal->type() );
        if( !tinfo )
            return nullopt;

        auto zexpr = tinfo->build( b, *loweredVal );



        return Z3Val { move( zexpr ), *ValueFromIRExpr( val.type() ) };
    }

    optional< Z3Val > BuildZ3ConstantFromType( Builder& b, const Value& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance()->getTypeInfo( b.context(), ValueToIRExpr( type ) );
        if( !tinfo )
            return nullopt;

        assert( tinfo->sort );
        return Z3Val { GetZ3Context().constant( name.c_str(), *tinfo->sort ), type };
    }

    optional< Z3Val > BuildZ3ConstantFromType( Builder& b, const Term& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance()->getTypeInfo( b.context(), type );
        if( !tinfo )
            return nullopt;

        assert( tinfo->sort );
        return Z3Val { GetZ3Context().constant( name.c_str(), *tinfo->sort ), *ValueFromIRExpr( type ) };
    }
︙︙
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193


194
195
196
197
198
199
200


    optional< Z3Val > BuildZ3Op( Builder& b, const GetTemporary& instr )
    {
        auto zv = b.retrieveVar( instr.index() );
        if( zv )
            return zv;

        return BuildZ3ConstantFromType( b.context(), instr.type(), format( "v{}", instr.index() ) );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const AllocVar& instr )
    {
        if( auto cst = BuildZ3ConstantFromType( b.context(), instr.type(), format( "v{}", b.newUniqueId() ) ) )
            b.setVar( instr.index(), move( *cst ) );

        return nullopt;


    }

    // Implemented in phi.cpp
    optional< Z3Val > BuildZ3Op( Builder& b, const Phi& instr );

    // TODO: LoadConstStr. Build a z3 str value.









|




|
<
|
|
>
>








175
176
177
178
179
180
181
182
183
184
185
186
187

188
189
190
191
192
193
194
195
196
197
198


    optional< Z3Val > BuildZ3Op( Builder& b, const GetTemporary& instr )
    {
        auto zv = b.retrieveVar( instr.index() );
        if( zv )
            return zv;

        return BuildZ3ConstantFromType( b, instr.type(), format( "v{}", instr.index() ) );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const AllocVar& instr )
    {
        auto tinfo = TypeCache::GetInstance()->getTypeInfo( b.context(), ValueToIRExpr( instr.type() ) );

        if( !tinfo )
            return nullopt;

        return Z3Val{ tinfo->undefined( b ), instr.type() };
    }

    // Implemented in phi.cpp
    optional< Z3Val > BuildZ3Op( Builder& b, const Phi& instr );

    // TODO: LoadConstStr. Build a z3 str value.
︙︙
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412


    optional< Z3Val > BuildZ3Op( Builder& b, const Placeholder& instr )
    {
        const auto* expr = b.retrievePlaceholder( instr.name() );
        if( expr )
            return Z3Val{ *expr, *ValueFromIRExpr( instr.type() ) };

        return BuildZ3ConstantFromType( b.context(), instr.type(), format( "p{}", instr.name() ) );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const llr::Instruction& instr )
    {
        return visit( [&]( auto&& e )
        {
            return BuildZ3Op( b, e );
        }, instr.content() );
    }

    optional< Z3Val > BuildZ3ExprFromValue( Builder& b, const Value& val )
    {
        if( val.isPoison() )
            return nullopt;

        if( val.isConstant() )
            return BuildZ3ValFromConstant( b.context(), val );

        if( auto expr = BuildZ3Op( b, *val.llr() )  )
            return expr;

        return BuildZ3ConstantFromType( b.context(), val.type(), format( "val{}", b.newUniqueId() ) );
    }
}








|
















|




|



379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410


    optional< Z3Val > BuildZ3Op( Builder& b, const Placeholder& instr )
    {
        const auto* expr = b.retrievePlaceholder( instr.name() );
        if( expr )
            return Z3Val{ *expr, *ValueFromIRExpr( instr.type() ) };

        return BuildZ3ConstantFromType( b, instr.type(), format( "p{}", instr.name() ) );
    }

    optional< Z3Val > BuildZ3Op( Builder& b, const llr::Instruction& instr )
    {
        return visit( [&]( auto&& e )
        {
            return BuildZ3Op( b, e );
        }, instr.content() );
    }

    optional< Z3Val > BuildZ3ExprFromValue( Builder& b, const Value& val )
    {
        if( val.isPoison() )
            return nullopt;

        if( val.isConstant() )
            return BuildZ3ValFromConstant( b, val );

        if( auto expr = BuildZ3Op( b, *val.llr() )  )
            return expr;

        return BuildZ3ConstantFromType( b, val.type(), format( "val{}", b.newUniqueId() ) );
    }
}
Changes to bs/verify/value.h.
︙︙
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

{
    struct Z3Val
    {
        z3::expr expr;
        ir::Value type;
    };

    extern optional< Z3Val > BuildZ3ValFromConstant( const sema::Context& c, const Value& val );
    extern optional< Z3Val > BuildZ3ExprFromValue( Builder& b, const Value& val );
    extern optional< Z3Val > BuildZ3ConstantFromType( const sema::Context& c, const Value& type, const string& name );
    extern optional< Z3Val > BuildZ3ConstantFromType( const sema::Context& c, const Term& type, const string& name );
    extern optional< Z3Val > BuildZ3Op( Builder& b, const llr::Instruction& instr );

    extern z3::expr GetAsBitVec( const z3::expr& expr, const Value& type );
    extern z3::expr GetAsBitVec( const Z3Val& zv );

    extern z3::expr GetAsInt( const z3::expr& expr, const Value& type );
    extern z3::expr GetAsInt( const Z3Val& zv );








|

|
|








8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

{
    struct Z3Val
    {
        z3::expr expr;
        ir::Value type;
    };

    extern optional< Z3Val > BuildZ3ValFromConstant( Builder& b, const Value& val );
    extern optional< Z3Val > BuildZ3ExprFromValue( Builder& b, const Value& val );
    extern optional< Z3Val > BuildZ3ConstantFromType( Builder& b, const Value& type, const string& name );
    extern optional< Z3Val > BuildZ3ConstantFromType( Builder& b, const Term& type, const string& name );
    extern optional< Z3Val > BuildZ3Op( Builder& b, const llr::Instruction& instr );

    extern z3::expr GetAsBitVec( const z3::expr& expr, const Value& type );
    extern z3::expr GetAsBitVec( const Z3Val& zv );

    extern z3::expr GetAsInt( const z3::expr& expr, const Value& type );
    extern z3::expr GetAsInt( const Z3Val& zv );
︙︙
Changes to tests/noprelude/verify/z3out-test-1.txt. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

=== Checking compilation-time call ===

=== Begin function verification trace ===
(= b1 true)
(= e1_2 (and b1 (distinct p0 5)))
(= b2 e1_2)
(= e1_3 (and b1 (not (distinct p0 5))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v31 p0))
(=> e2_3 (= v31 5))
check_unsat (and b3 (not (= v31 5)))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
=== End function verification trace ===











|
|
|







1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

=== Checking compilation-time call ===

=== Begin function verification trace ===
(= b1 true)
(= e1_2 (and b1 (distinct p0 5)))
(= b2 e1_2)
(= e1_3 (and b1 (not (distinct p0 5))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v30 p0))
(=> e2_3 (= v30 5))
check_unsat (and b3 (not (= v30 5)))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
=== End function verification trace ===
Changes to tests/noprelude/verify/z3out-test-2.txt. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Begin function verification trace ===
assume (distinct p0 p1)
(= b1 true)
(= e1_2 (and b1 (< p0 p1)))
(= b2 e1_2)
(=> e1_2 (= v35 p1))
(=> e1_2 (= v37 p0))
(= e1_3 (and b1 (not (< p0 p1))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v38 p0))
(=> e2_3 (= v38 v35))
(=> e1_3 (= v39 p1))
(=> e2_3 (= v39 v37))
check_unsat (and b3 (not (> v38 v39)))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
check_unsat (not (distinct 2 1))
=== End function verification trace ===











|
|



|
|
|
|
|








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Begin function verification trace ===
assume (distinct p0 p1)
(= b1 true)
(= e1_2 (and b1 (< p0 p1)))
(= b2 e1_2)
(=> e1_2 (= v34 p1))
(=> e1_2 (= v36 p0))
(= e1_3 (and b1 (not (< p0 p1))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v37 p0))
(=> e2_3 (= v37 v34))
(=> e1_3 (= v38 p1))
(=> e2_3 (= v38 v36))
check_unsat (and b3 (not (> v37 v38)))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
check_unsat (not (distinct 2 1))
=== End function verification trace ===
Changes to tests/noprelude/verify/z3out-test-3.txt. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Begin function verification trace ===
assume (distinct p0 p1)
(= b1 true)
(= e1_2 (and b1 (< p0 p1)))
(= b2 e1_2)
(=> e1_2 (= v35 p1))
(=> e1_2 (= v37 p0))
(= e1_3 (and b1 (not (< p0 p1))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v38 p0))
(=> e2_3 (= v38 v35))
(=> e1_3 (= v39 p1))
(=> e2_3 (= v39 v37))
check_unsat (and b3 (not (> (- v38 v39) 0)))
=== End function verification trace ===

=== Checking compilation-time call ===
check_unsat (not (distinct 2 1))

=== Begin function verification trace ===
(= b1 true)












|
|



|
|
|
|
|








1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Begin function verification trace ===
assume (distinct p0 p1)
(= b1 true)
(= e1_2 (and b1 (< p0 p1)))
(= b2 e1_2)
(=> e1_2 (= v34 p1))
(=> e1_2 (= v36 p0))
(= e1_3 (and b1 (not (< p0 p1))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v37 p0))
(=> e2_3 (= v37 v34))
(=> e1_3 (= v38 p1))
(=> e2_3 (= v38 v36))
check_unsat (and b3 (not (> (- v37 v38) 0)))
=== End function verification trace ===

=== Checking compilation-time call ===
check_unsat (not (distinct 2 1))

=== Begin function verification trace ===
(= b1 true)
︙︙
Changes to tests/noprelude/verify/z3out-test-4.txt.
︙︙
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

=== Checking compilation-time call ===

=== Begin function verification trace ===
assume (distinct p0 p1)
(= b1 true)
(= e1_2 (and b1 (< p0 p1)))
(= b2 e1_2)
(=> e1_2 (= v35 p1))
(=> e1_2 (= v37 p0))
(= e1_3 (and b1 (not (< p0 p1))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v38 p0))
(=> e2_3 (= v38 v35))
(=> e1_3 (= v39 p1))
(=> e2_3 (= v39 v37))
check_unsat (and b3 (not (> (- v38 v39) 0)))
=== End function verification trace ===

=== Begin function verification trace ===
assume (distinct p0 0)
(= b1 true)
check_unsat (not (distinct p0 (* 2 p0)))
assume (> r40 0)
check_unsat (not (distinct r40 0))
=== End function verification trace ===

=== Checking compilation-time call ===
check_unsat (not (distinct 5 0))

=== Begin function verification trace ===
(= b1 true)








|
|



|
|
|
|
|






|
|








9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

=== Checking compilation-time call ===

=== Begin function verification trace ===
assume (distinct p0 p1)
(= b1 true)
(= e1_2 (and b1 (< p0 p1)))
(= b2 e1_2)
(=> e1_2 (= v34 p1))
(=> e1_2 (= v36 p0))
(= e1_3 (and b1 (not (< p0 p1))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v37 p0))
(=> e2_3 (= v37 v34))
(=> e1_3 (= v38 p1))
(=> e2_3 (= v38 v36))
check_unsat (and b3 (not (> (- v37 v38) 0)))
=== End function verification trace ===

=== Begin function verification trace ===
assume (distinct p0 0)
(= b1 true)
check_unsat (not (distinct p0 (* 2 p0)))
assume (> r39 0)
check_unsat (not (distinct r39 0))
=== End function verification trace ===

=== Checking compilation-time call ===
check_unsat (not (distinct 5 0))

=== Begin function verification trace ===
(= b1 true)
︙︙
Changes to tests/noprelude/verify/z3out-test-logic-and.txt. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

=== Begin function verification trace ===
(= b1 true)
(= e1_2 (and b1 false))
(= b2 e1_2)
(=> e1_2 (= v32 true))
(= e1_3 (and b1 (not false)))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v33 false))
(=> e2_3 (= v34 v32))
(=> e2_3 (= v33 v34))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
=== End function verification trace ===






|



|
|
|







1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

=== Begin function verification trace ===
(= b1 true)
(= e1_2 (and b1 false))
(= b2 e1_2)
(=> e1_2 (= v31 true))
(= e1_3 (and b1 (not false)))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v32 false))
(=> e2_3 (= v33 v31))
(=> e2_3 (= v32 v33))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
=== End function verification trace ===
Changes to tests/noprelude/verify/z3out-test-logic-or.txt. 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

=== Begin function verification trace ===
(= b1 true)
(= e1_2 (and b1 (not false)))
(= b2 e1_2)
(=> e1_2 (= v32 true))
(= e1_3 (and b1 false))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v33 true))
(=> e2_3 (= v34 v32))
(=> e2_3 (= v33 v34))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
=== End function verification trace ===






|



|
|
|







1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

=== Begin function verification trace ===
(= b1 true)
(= e1_2 (and b1 (not false)))
(= b2 e1_2)
(=> e1_2 (= v31 true))
(= e1_3 (and b1 false))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v32 true))
(=> e2_3 (= v33 v31))
(=> e2_3 (= v32 v33))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
=== End function verification trace ===
Fossil 2.26 [1205ec86cb] 2025-04-30 16:57:32
This page was generated in about 0.03s