Goose  Diff

Annotate Patch Side-by-side Diff

Differences From Artifact [1dd876e35a]:

  • File bs/verify/value.cpp — part of check-in [57d4d0c79e] at 2024-09-13 21:05:40 on branch cir-ssa-refactor — Drop in the most apocalyptic changes: new CIR instruction structure, new sequence builder, new compile time address representation, do almost just the bare minimum to compile again. A few simple things are still working somehow (user: achavasse size: 24047)

To Artifact [fb0a11cf9c]:

  • File bs/verify/value.cpp — part of check-in [0db147f117] at 2024-09-15 20:24:31 on branch cir-ssa-refactor — Add clang format settings, reformat everything (user: achavasse size: 24683)
︙
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
75
76
77
78

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

75
76
77
78
79
80
81
82
83








-
+









-
+









-
+
+


-
+
+






-
+
+










-
+
+










-
+
+









        tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), val.type() );

        if( !tinfo )
            tinfo = TypeCache::GetInstance().uninterpretedTypeInfo();

        auto zexpr = tinfo->build( b, val );
        return Z3Val { move( zexpr ), *EIRToValue( val.type() ), val.locationId() };
        return Z3Val{ move( zexpr ), *EIRToValue( val.type() ), val.locationId() };
    }

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

        auto zexpr = tinfo->build( b, val );
        return Z3Val { move( zexpr ), *EIRToValue( val.type() ), val.locationId() };
        return Z3Val{ move( zexpr ), *EIRToValue( val.type() ), val.locationId() };
    }

    Z3Val BuildZ3ConstantFromType( Builder& b, const Value& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), ValueToEIR( type ) );
        if( !tinfo )
            tinfo = TypeCache::GetInstance().uninterpretedTypeInfo();

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

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

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

    Z3Val BuildZ3ConstantFromType( Builder& b, const Term& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), type );
        if( !tinfo )
            tinfo = TypeCache::GetInstance().uninterpretedTypeInfo();

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

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

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

    z3::expr GetAsBitVec( const z3::expr& expr, const Value& type )
    {
        if( expr.is_bv() )
            return expr;
︙
118
119
120
121
122
123
124
125

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
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
198
199
200
201
202
203
204
205


206
207
208
209
210
211


212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231


232
233
234
235
236
237
238
239
240


241
242
243
244
245
246
247


248
249
250
251
252
253
254

123
124
125
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
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
198
199
200
201
202
203
204

205
206
207
208
209
210
211
212
213

214
215
216
217
218
219
220

221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241

242
243
244
245
246
247
248
249
250
251

252
253
254
255
256
257
258
259

260
261
262
263
264
265
266
267
268








-
+
-









-
+
-











+
-
+








-
+
+





-
+
+



















-
+
+





-
+
+





+
-
+








-
+
+





-
+
+



















-
+
+








-
+
+






-
+
+








            return GetAsInt( expr, to.type );
        else if( to.expr.is_bv() )
            return GetAsBitVec( expr, to.type );
        else
            return expr;
    }

    template< typename I, typename F >
    template< typename I, typename F > bool BuildZ3UnaryExpr( Builder& b, const I& instr, F&& func )
    bool BuildZ3UnaryExpr( Builder& b, const I& instr, F&& func )
    {
        auto operand = b.pop();
        if( !operand )
            return false;

        b.push( Z3Val{ func( operand->expr ), operand->type, instr.locationId() } );
        return true;
    }

    template< typename I, typename F >
    template< typename I, typename F > bool BuildZ3BinExpr( Builder& b, const I& instr, F&& func )
    bool BuildZ3BinExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

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

        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
        {
            b.push(
            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
                Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
            return true;
        }

        // If we are trying to do an operation on a mix of bitvec and int,
        // convert the int to a bitvec first.
        if( lhs->expr.is_bv() )
        {
            assert( rhs->expr.is_int() );
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type, instr.locationId() } );
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type,
                instr.locationId() } );
            return true;
        }
        else
        {
            assert( lhs->expr.is_int() );
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type,
                instr.locationId() } );
            return true;
        }

        return false;
    }

    template< typename I, typename F >
    bool BuildZ3BinBitwiseExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

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

        if( ValueToEIR( lhs->type ) == GetValueType< BigInt >() )
        {
            DiagnosticsManager::GetInstance().emitErrorMessage( 0, "verifier error: bitwise operands can't be ct_int." );
            DiagnosticsManager::GetInstance().emitErrorMessage(
                0, "verifier error: bitwise operands can't be ct_int." );
            return false;
        }

        if( ValueToEIR( rhs->type ) == GetValueType< BigInt >() )
        {
            DiagnosticsManager::GetInstance().emitErrorMessage( 0, "verifier error: bitwise operands can't be ct_int." );
            DiagnosticsManager::GetInstance().emitErrorMessage(
                0, "verifier error: bitwise operands can't be ct_int." );
            return false;
        }

        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
        {
            b.push(
            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
                Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
            return true;
        }

        // If we are trying to do an operation on a mix of bitvec and int,
        // convert the int to a bitvec first.
        if( lhs->expr.is_bv() )
        {
            assert( rhs->expr.is_int() );
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type, instr.locationId() } );
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type,
                instr.locationId() } );
            return true;
        }
        else
        {
            assert( lhs->expr.is_int() );
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type,
                instr.locationId() } );
            return true;
        }

        return false;
    }

    template< typename I, typename F >
    bool BuildZ3BinBoolExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

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

        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
        {
            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ),
                *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
            return true;
        }

        // If we are trying to do an operation on a mix of bitvec and int,
        // convert the int to a bitvec first.
        if( lhs->expr.is_bv() )
        {
            assert( rhs->expr.is_int() );
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ),
                *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
            return true;
        }
        else
        {
            cout << lhs->expr << endl;
            assert( lhs->expr.is_int() );
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ),
                *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
            return true;
        }

        return false;
    }

    template< typename I, typename F >
︙
264
265
266
267
268
269
270
271


272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294

295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311

312
313
314
315
316
317
318
319
320
321
322
323
324

325

326
327
328
329
330
331

332
333

334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361












362
363
364
365
366
367
368

278
279
280
281
282
283
284

285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306



307
308
309
310
311
312
313
314

315
316

317
318
319
320


321
322
323
324
325
326
327
328
329
330
331
332
333
334
335

336
337
338
339
340
341

342


343

344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359











360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378








-
+
+




















-
-
-
+







-


-




-
-
+













+
-
+





-
+
-
-
+
-
















-
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+









        if( !lhs->expr.is_bool() )
            return false;

        if( !rhs->expr.is_bool() )
            return false;

        b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
        b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ),
            *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
        return true;
    }

    template< typename RT, typename I, typename F >
    bool BuildZ3BinSeqExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

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

        if( !lhs->expr.is_seq() )
            return false;

        if( !rhs->expr.is_seq() )
            return false;

        b.push( Z3Val{
            func( lhs->expr, rhs->expr ),
            *EIRToValue( GetValueType< RT >() ),
        b.push( Z3Val{ func( lhs->expr, rhs->expr ), *EIRToValue( GetValueType< RT >() ),
            instr.locationId() } );
        return true;
    }

    bool BuildZ3Op( Builder& b, const cir::InstrSeq& is )
    {
        for( const auto& instr : is )
        {
            if( !BuildZ3Op( b, instr ) )
                return false;
        }

        return true;
    }

    template< typename T >
    bool BuildZ3Op( Builder& b, const T& instr )
    template< typename T > bool BuildZ3Op( Builder& b, const T& instr )
    {
        return false;
    }

    bool BuildZ3Op( Builder& b, const Load& instr )
    {
        optional< Z3Val > zv;

        if( auto cstAddr = b.pop< Address >() )
            zv = LoadFromAddress( b, *cstAddr, instr.type().get() );
        else if( auto gfa = b.pop< GhostFuncApplication >() )
            zv = LoadFromAddress( b, *gfa );
        else if( auto symAddr = b.pop< Z3Val >() )
            zv = BuildZ3ConstantFromType(
            zv = BuildZ3ConstantFromType( b, instr.type().get(), format( "val{}", b.newUniqueId() ) );
                b, instr.type().get(), format( "val{}", b.newUniqueId() ) );

        if( !zv )
            return false;

        if( b.mustLoadAssume() )
            ForEachPredicate( b, instr.type().get(), zv->expr, [&]( auto&& z3expr, auto locId )
            ForEachPredicate( b, instr.type().get(), zv->expr,
            {
                b.assume( z3expr );
                [&]( auto&& z3expr, auto locId ) { b.assume( z3expr ); } );
            } );

        zv->loc = instr.locationId();
        b.push( move( *zv ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const Store& instr )
    {
        auto addr = b.pop< Stack::Slot >();
        if( !addr )
            return false;

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

        ForEachPredicate( b, instr.type().get(), zv->expr, [&]( auto&& z3expr, auto locId )
        {
            if( !instr.srcLocId().invalid() && !instr.destLocId().invalid() )
            {
                DiagnosticsContext dc( instr.destLocId(), "...to this." );
                DiagnosticsContext dc2( instr.srcLocId(), "When assigning this..." );
                b.checkAssertion( z3expr, locId );
            }
            else
                b.checkAssertion( z3expr, locId );
        } );
        ForEachPredicate( b, instr.type().get(), zv->expr,
            [&]( auto&& z3expr, auto locId )
            {
                if( !instr.srcLocId().invalid() && !instr.destLocId().invalid() )
                {
                    DiagnosticsContext dc( instr.destLocId(), "...to this." );
                    DiagnosticsContext dc2( instr.srcLocId(), "When assigning this..." );
                    b.checkAssertion( z3expr, locId );
                }
                else
                    b.checkAssertion( z3expr, locId );
            } );

        if( const auto* cstAddr = get_if< Address >( &*addr ) )
            StoreToAddress( b, *cstAddr, move( *zv ) );
        else if( const auto* gfa = get_if< GhostFuncApplication >( &*addr ) )
            StoreToAddress( b, *gfa, move( *zv ) );

        return true;
︙
394
395
396
397
398
399
400

401

402
403
404
405
406
407
408
409
410
411
412
413





414
415
416
417



418
419
420
421
422
423
424
425





426
427
428
429
430




431
432
433
434
435
436
437
438





439
440
441
442
443




444
445
446
447
448
449
450
451





452
453
454
455
456




457
458
459
460
461

462
463

464
465
466
467
468
469

470
471

472
473
474
475
476
477
478
479
480
481
482







483
484
485
486
487
488
489
490
491
492







493
494
495
496
497
498
499
500
501
502







503
504
505
506

507

508
509
510
511

512

513
514
515
516

517

518
519
520
521

522

523
524
525
526

527

528
529
530
531

532

533
534
535
536
537
538
539
540





541
542
543


544
545
546
547

548

549
550
551
552

553

554
555
556
557

558

559
560
561
562

563

564
565
566
567

568

569
570
571
572

573

574
575
576
577

578

579
580
581
582

583

584
585
586
587

588

589
590
591
592

593

594
595
596
597
598
599
600

404
405
406
407
408
409
410
411

412
413
414
415
416
417
418
419
420




421
422
423
424
425
426



427
428
429
430
431
432
433




434
435
436
437
438
439




440
441
442
443
444
445
446
447




448
449
450
451
452
453




454
455
456
457
458
459
460
461




462
463
464
465
466
467




468
469
470
471
472
473
474
475

476


477

478
479
480
481

482


483

484
485
486
487






488
489
490
491
492
493
494
495
496
497
498






499
500
501
502
503
504
505
506
507
508
509






510
511
512
513
514
515
516
517
518
519
520
521

522
523
524
525
526
527

528
529
530
531
532
533

534
535
536
537
538
539

540
541
542
543
544
545

546
547
548
549
550
551

552
553
554
555
556




557
558
559
560
561
562


563
564
565
566
567
568
569

570
571
572
573
574
575

576
577
578
579
580
581

582
583
584
585
586
587

588
589
590
591
592
593

594
595
596
597
598
599

600
601
602
603
604
605

606
607
608
609
610
611

612
613
614
615
616
617

618
619
620
621
622
623

624
625
626
627
628
629
630
631








+
-
+








-
-
-
-
+
+
+
+
+

-
-
-
+
+
+




-
-
-
-
+
+
+
+
+

-
-
-
-
+
+
+
+




-
-
-
-
+
+
+
+
+

-
-
-
-
+
+
+
+




-
-
-
-
+
+
+
+
+

-
-
-
-
+
+
+
+




-
+
-
-
+
-




-
+
-
-
+
-




-
-
-
-
-
-
+
+
+
+
+
+
+




-
-
-
-
-
-
+
+
+
+
+
+
+




-
-
-
-
-
-
+
+
+
+
+
+
+




+
-
+




+
-
+




+
-
+




+
-
+




+
-
+




+
-
+




-
-
-
-
+
+
+
+
+

-
-
+
+




+
-
+




+
-
+




+
-
+




+
-
+




+
-
+




+
-
+




+
-
+




+
-
+




+
-
+




+
-
+









    bool BuildZ3Op( Builder& b, const AllocVar& instr )
    {
        auto tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), instr.type().get() );
        if( !tinfo )
            tinfo = TypeCache::GetInstance().uninterpretedTypeInfo();

        b.setVar( instr.index(),
        b.setVar( instr.index(), Z3Val{ tinfo->undefined( b ), *EIRToValue( instr.type().get() ), instr.locationId() } );
            Z3Val{ tinfo->undefined( b ), *EIRToValue( instr.type().get() ), instr.locationId() } );
        return true;
    }

    // Implemented in phi.cpp
    bool BuildZ3Op( Builder& b, const Phi& instr );

    bool BuildZ3Op( Builder& b, const Not& instr )
    {
        return BuildZ3UnaryExpr( b, instr, []( auto&& operand )
        {
            if( operand.is_bool() )
                return !operand;
        return BuildZ3UnaryExpr( b, instr,
            []( auto&& operand )
            {
                if( operand.is_bool() )
                    return !operand;

            assert( operand.is_bv() );
            return ~operand;
        } );
                assert( operand.is_bv() );
                return ~operand;
            } );
    }

    bool BuildZ3Op( Builder& b, const And& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bool() && rhs.is_bool() )
                return lhs && rhs;
        return BuildZ3BinBitwiseExpr( b, instr,
            []( auto&& lhs, auto&& rhs, auto&& type )
            {
                if( lhs.is_bool() && rhs.is_bool() )
                    return lhs && rhs;

            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return lhsBV & rhsBV;
        } );
                auto lhsBV = GetAsBitVec( lhs, type );
                auto rhsBV = GetAsBitVec( rhs, type );
                return lhsBV & rhsBV;
            } );
    }

    bool BuildZ3Op( Builder& b, const Or& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bool() && rhs.is_bool() )
                return lhs || rhs;
        return BuildZ3BinBitwiseExpr( b, instr,
            []( auto&& lhs, auto&& rhs, auto&& type )
            {
                if( lhs.is_bool() && rhs.is_bool() )
                    return lhs || rhs;

            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return lhsBV | rhsBV;
        } );
                auto lhsBV = GetAsBitVec( lhs, type );
                auto rhsBV = GetAsBitVec( rhs, type );
                return lhsBV | rhsBV;
            } );
    }

    bool BuildZ3Op( Builder& b, const Xor& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bool() && rhs.is_bool() )
                return lhs ^ rhs;
        return BuildZ3BinBitwiseExpr( b, instr,
            []( auto&& lhs, auto&& rhs, auto&& type )
            {
                if( lhs.is_bool() && rhs.is_bool() )
                    return lhs ^ rhs;

            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return lhsBV ^ rhsBV;
        } );
                auto lhsBV = GetAsBitVec( lhs, type );
                auto rhsBV = GetAsBitVec( rhs, type );
                return lhsBV ^ rhsBV;
            } );
    }

    bool BuildZ3Op( Builder& b, const Implies& instr )
    {
        return BuildZ3BinLogicExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        return BuildZ3BinLogicExpr( b, instr,
        {
            return z3::implies( lhs, rhs );
            []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::implies( lhs, rhs ); } );
        } );
    }

    bool BuildZ3Op( Builder& b, const IsPrefixOf& instr )
    {
        return BuildZ3BinSeqExpr< bool >( b, instr, []( auto&& lhs, auto&& rhs )
        return BuildZ3BinSeqExpr< bool >(
        {
            return z3::prefixof( lhs, rhs );
            b, instr, []( auto&& lhs, auto&& rhs ) { return z3::prefixof( lhs, rhs ); } );
        } );
    }

    bool BuildZ3Op( Builder& b, const Shl& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return z3::shl( lhsBV, rhsBV );
        } );
        return BuildZ3BinBitwiseExpr( b, instr,
            []( auto&& lhs, auto&& rhs, auto&& type )
            {
                auto lhsBV = GetAsBitVec( lhs, type );
                auto rhsBV = GetAsBitVec( rhs, type );
                return z3::shl( lhsBV, rhsBV );
            } );
    }

    bool BuildZ3Op( Builder& b, const LShr& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return z3::lshr( lhsBV, rhsBV );
        } );
        return BuildZ3BinBitwiseExpr( b, instr,
            []( auto&& lhs, auto&& rhs, auto&& type )
            {
                auto lhsBV = GetAsBitVec( lhs, type );
                auto rhsBV = GetAsBitVec( rhs, type );
                return z3::lshr( lhsBV, rhsBV );
            } );
    }

    bool BuildZ3Op( Builder& b, const AShr& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return z3::ashr( lhsBV, rhsBV );
        } );
        return BuildZ3BinBitwiseExpr( b, instr,
            []( auto&& lhs, auto&& rhs, auto&& type )
            {
                auto lhsBV = GetAsBitVec( lhs, type );
                auto rhsBV = GetAsBitVec( rhs, type );
                return z3::ashr( lhsBV, rhsBV );
            } );
    }

    bool BuildZ3Op( Builder& b, const Add& instr )
    {
        return BuildZ3BinExpr(
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs + rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs + rhs; } );
    }

    bool BuildZ3Op( Builder& b, const Sub& instr )
    {
        return BuildZ3BinExpr(
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs - rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs - rhs; } );
    }

    bool BuildZ3Op( Builder& b, const Mul& instr )
    {
        return BuildZ3BinExpr(
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs * rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs * rhs; } );
    }

    bool BuildZ3Op( Builder& b, const UDiv& instr )
    {
        return BuildZ3BinExpr(
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::udiv( lhs, rhs ); } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::udiv( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const SDiv& instr )
    {
        return BuildZ3BinExpr(
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs / rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs / rhs; } );
    }

    bool BuildZ3Op( Builder& b, const URem& instr )
    {
        return BuildZ3BinExpr(
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::urem( lhs, rhs ); } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::urem( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const SRem& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bv() )
                return z3::srem( lhs, rhs );
        return BuildZ3BinExpr( b, instr,
            []( auto&& lhs, auto&& rhs, auto&& type )
            {
                if( lhs.is_bv() )
                    return z3::srem( lhs, rhs );

            return z3::rem( lhs, rhs );
        } );
                return z3::rem( lhs, rhs );
            } );
    }

    bool BuildZ3Op( Builder& b, const Eq& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs == rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs == rhs; } );
    }

    bool BuildZ3Op( Builder& b, const Neq& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs != rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs != rhs; } );
    }

    bool BuildZ3Op( Builder& b, const UGT& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ugt( lhs, rhs ); } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ugt( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const UGE& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::uge( lhs, rhs ); } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::uge( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const ULT& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ult( lhs, rhs ); } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ult( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const ULE& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ule( lhs, rhs ); } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ule( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const SGT& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs > rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs > rhs; } );
    }

    bool BuildZ3Op( Builder& b, const SGE& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs >= rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs >= rhs; } );
    }

    bool BuildZ3Op( Builder& b, const SLT& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs < rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs < rhs; } );
    }

    bool BuildZ3Op( Builder& b, const SLE& instr )
    {
        return BuildZ3BinBoolExpr(
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs <= rhs; } );
            b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs <= rhs; } );
    }

    bool BuildZ3Op( Builder& b, const Assert& instr )
    {
        auto cond = b.pop();
        if( !cond )
            return false;
︙
608
609
610
611
612
613
614

615

616
617
618
619
620
621
622

639
640
641
642
643
644
645
646

647
648
649
650
651
652
653
654








+
-
+








        const auto* expr = b.retrievePlaceholder( instr.name() );
        if( expr )
        {
            b.push( Z3Val{ *expr, *EIRToValue( instr.type().get() ), instr.locationId() } );
            return true;
        }

        auto result =
        auto result = BuildZ3ConstantFromType( b, instr.type().get(), format( "p{}", instr.name().str() ) );
            BuildZ3ConstantFromType( b, instr.type().get(), format( "p{}", instr.name().str() ) );
        b.push( move( result ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const PHOverrideSet& instr )
    {
        auto phExpr = b.pop();
︙
658
659
660
661
662
663
664

665

666
667
668
669
670
671
672
673
674
675
676
677
678
679

680
681

682
683
684

685
686
687

688
689
690
691
692
693
694
695
696

690
691
692
693
694
695
696
697

698
699
700
701
702
703
704
705
706
707
708
709
710
711

712


713



714

715

716


717
718
719
720
721
722
723








+
-
+













-
+
-
-
+
-
-
-
+
-

-
+
-
-








        return !!b.setVar( instr.tempIndex(), move( *initVal ) );
    }

    bool BuildZ3Op( Builder& b, const Select& instr )
    {
        if( auto cstBaseLoc = b.pop< Address >() )
        {
            b.push(
            b.push( Address::Select( move( *cstBaseLoc ), instr.memberIndex(), instr.locationId() ) );
                Address::Select( move( *cstBaseLoc ), instr.memberIndex(), instr.locationId() ) );
            return true;
        }

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

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

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

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

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

        return true;
    }

    bool BuildZ3Op( Builder& b, const GhostCall& instr )
    {
        auto gfunc = b.pop< Value >();
︙
767
768
769
770
771
772
773
774

775
776
777
778
779
780
781
782
783
784

794
795
796
797
798
799
800

801



802
803
804
805
806
807
808








-
+
-
-
-








    {
        G_ERROR( "InlineCall encountered during verification" );
        return false;
    }

    bool BuildZ3Op( Builder& b, const cir::Instruction& instr )
    {
        return visit( [&]( auto&& e )
        return visit( [&]( auto&& e ) { return BuildZ3Op( b, e ); }, instr );
        {
            return BuildZ3Op( b, e );
        }, instr );
    }

    Z3Val BuildZ3ExprFromValue( Builder& b, const Value& val )
    {
        if( val.isConstant() )
            return BuildZ3ValFromConstant( b, val );
︙
801
802
803
804
805
806
807
808


825
826
827
828
829
830
831

832








-
+

            return TryBuildZ3ValFromConstant( b, val );

        if( BuildZ3Op( b, *val.cir() ) )
            return b.pop();

        return TryBuildZ3ConstantFromType( b, val.type(), format( "val{}", b.newUniqueId() ) );
    }
}
} // namespace goose::verify
Fossil 2.26 [1205ec86cb] 2025-04-30 16:57:32
This page was generated in about 0.015s