Goose  Diff

Differences From Artifact [05b81fc021]:

  • File bs/verify/value.cpp — part of check-in [08898dae70] at 2023-06-17 10:15:09 on branch trunk —
    • Remove MemLoc, it's redundant with cir::Address
    • Added compîlation time sequence type
    • Partially handle sequence type in the verifier (to be completed later)
    • Added "SelectPath" builtin type for adress paths
    (user: zlodo size: 22249)

To Artifact [03f3fd8fe9]:

  • File bs/verify/value.cpp — part of check-in [1adbcaa805] at 2023-06-30 22:41:22 on branch trunk — Verifier:
    • Remove hardcoded handling of ref type from verifier, lower ref type to address for verification instead
    • Complete the handling of address type and handle selecting+loading an address' lifetime, origin and path
    (user: zlodo size: 22340)

643
644
645
646
647
648
649
650
651



652
653
654
655

656

657
658
659
660
661
662
663
643
644
645
646
647
648
649


650
651
652
653
654
655

656
657
658
659
660
661
662
663
664
665







-
-
+
+
+



-
+

+








        auto symBaseLoc = b.pop();
        if( !symBaseLoc )
            return false;

        const auto& tc = TypeCache::GetInstance();

        auto ltExpr = tc.memLocLifetimeGetter()( symBaseLoc->expr );
        auto pathExpr = tc.memLocPathGetter()( symBaseLoc->expr );
        auto ltExpr = tc.addrLifetimeGetter()( symBaseLoc->expr );
        auto originExpr = tc.addrOriginGetter()( symBaseLoc->expr );
        auto pathExpr = tc.addrPathGetter()( symBaseLoc->expr );

        b.push( Z3Val
        {
            tc.memLocCtor()(
            tc.addrCtor()(
                ltExpr,
                originExpr,
                z3::concat( pathExpr, GetZ3Context().int_val( instr.memberIndex() ).unit() )
            ),

            *EIRToValue( GetValueType< cir::Address >() ),
            instr.locationId()
        } );