Fix: Check non-exhaustible conditional returns using a `goto` mechanism #75

divyaranjan1905 · 2025-10-16T09:36:02Z

Fixes #54.

I've added a goto mechanism, that adds explicit jump instructions to handle early returns in inlined functions. When an inline function has a return statement inside a conditional branch that doesn't cover all code paths, the mechanism ensures that execution jumps to the end of the inlined function body (the "epilogue") instead of continuing to execute subsequent code.

The mechanism operates at two levels:

At the Line level (during inlining): When inline_lines() encounters a Line::FunctionRet statement, it now:

Converts the return into assignments (as before)
Inserts a Line::Goto instruction that jumps to a unique epilogue label (e.g.,@inline_epilogue_0)

At the SimpleLine level (during simplification): The Line::Goto is converted to SimpleLine::Goto when the program is simplified.
At the intermediate bytecode level: The SimpleLine::Goto compiles to an unconditional IntermediateInstruction::Jump to the epilogue label, and the remaining code after the goto is registered in the bytecode map with that label.

Running the previously buggy inline_bug_mre test with print statements enabled in lib.rs, we get:

[divya@archdivya leanMultisig]$ RUST_BACKTRACE=1 cargo test -p lean_compiler inline_bug_mre -- --nocapture
    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.04s
     Running unittests src/lib.rs (target/debug/deps/lean_compiler-a1c9bc5cce5d53bb)

running 0 tests

test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 3 filtered out; finished in 0.00s

     Running tests/test_compiler.rs (target/debug/deps/test_compiler-bc0011693c4ca4dc)

running 1 test
Parsed program: fn boolean(a) -> 0 {
    
    if a == 0 {
        
        return 0
    }
    
    return 1
}
fn main() -> 0 {
    
    x = boolean(0)
    
    return 
}
Simplified program: fn main() -> 0 {
    
    
    @diff_0 = 0 - 0
    if @diff_0 != 0 {

    } else {
        
        x = 0 + 0
        goto_@inline_epilogue_0
    }
    
    x = 1 + 0
    goto_@inline_epilogue_0
    
    return 
}
Intermediate Bytecode:


@function_main:
  
  
  0 = m[fp + 2] + 0
  m[fp + 4] = inverse(m[fp + 2])
  m[fp + 5] = m[fp + 2] x m[fp + 4]
  1 = m[fp + 6] + m[fp + 5]
  0 = m[fp + 6] x m[fp + 2]
  jump_if_not_zero m[fp + 5] to @if_0
  jump @else_0

@if_0:
  jump @if_else_end_0

@else_0:
  
  m[fp + 3] = 0 + 0
  jump @inline_epilogue_0

@if_else_end_0:
  
  m[fp + 3] = 1 + 0
  jump @inline_epilogue_0

@inline_epilogue_0:
  
  m[fp + 7] = 0 + 0
  jump @end_program with fp = m[fp + 7]

Memory size per function:
main: 8

Function Locations: 

main: 2
boolean: 7


Compiled Program:

hint: label: @function_main
hint: source line number: 3
hint: source line number: 8
   0: 0 = 0 + m[fp + 2]
hint: m[fp + 4] = inverse(m[fp + 2])
   1: m[fp + 5] = m[fp + 2] x m[fp + 4]
   2: 1 = m[fp + 6] + m[fp + 5]
   3: 0 = m[fp + 6] x m[fp + 2]
   4: if m[fp + 5] != 0 jump to @if_0 = 7 with next(fp) = fp
   5: if 1 != 0 jump to @else_0 = 8 with next(fp) = fp
hint: label: @end_program
   6: if 1 != 0 jump to @end_program = 6 with next(fp) = fp
hint: label: @if_0
   7: if 1 != 0 jump to @if_else_end_0 = 10 with next(fp) = fp
hint: label: @else_0
hint: source line number: 9
   8: 0 = 0 + m[fp + 3]
   9: if 1 != 0 jump to @inline_epilogue_0 = 12 with next(fp) = fp
hint: label: @if_else_end_0
hint: source line number: 11
  10: 1 = 0 + m[fp + 3]
  11: if 1 != 0 jump to @inline_epilogue_0 = 12 with next(fp) = fp
hint: label: @inline_epilogue_0
hint: source line number: 4
  12: 0 = 0 + m[fp + 7]
  13: if 1 != 0 jump to @end_program = 6 with next(fp) = m[fp + 7]

╔═════════════════════════════════════════════════════════════════════════╗
║                                 STATS                                   ║
╚═════════════════════════════════════════════════════════════════════════╝

CYCLES: 10
MEMORY: 73

Bytecode size: 14
Public input size: 0
Private input size: 0
Runtime memory: 25 (0.00% vec) (no vec mem: 0)
Memory usage: 88.0%

──────────────────────────────────────────────────────────────────────────

test inline_bug_mre ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 19 filtered out; finished in 0.00s

[divya@archdivya leanMultisig]$

…lation Also uncomments the inline_bug_mre test

divyaranjan1905 · 2025-10-16T09:45:40Z

I tried a few other tests from #65. Starting with the one @TomWambsgans recommended:

[divya@archdivya leanMultisig]$ RUST_BACKTRACE=1 cargo test -p lean_compiler test_doesnt_work -- --nocapture
   Compiling lean_compiler v0.1.0 (/home/divya/src/leanMultisig/crates/lean_compiler)
    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.19s
     Running unittests src/lib.rs (target/debug/deps/lean_compiler-1a2d7a131c613260)

running 0 tests

test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 3 filtered out; finished in 0.00s

     Running tests/test_compiler.rs (target/debug/deps/test_compiler-c47d8cf7d224f8c7)

running 1 test
Parsed program: fn doesnt_work(x) -> 1 {
    
    if x == 1 {
        
        if x == 0 {
            
            return 100
        }
        
        if x == 1 {
            
            return 200
        }
    }
    
    return 300
}
fn main() -> 0 {
    
    b = doesnt_work(1)
    
    print(b)
    
    return 
}
Simplified program: fn main() -> 0 {
    
    
    @diff_0 = 1 - 1
    if @diff_0 != 0 {

    } else {
        
        @diff_1 = 1 - 0
        if @diff_1 != 0 {

        } else {
            
            b = 100 + 0
            goto_@inline_epilogue_0
        }
        
        @diff_2 = 1 - 1
        if @diff_2 != 0 {

        } else {
            
            b = 200 + 0
            goto_@inline_epilogue_0
        }
    }
    
    b = 300 + 0
    goto_@inline_epilogue_0
    
    print(b)
    
    return 
}
Intermediate Bytecode:


@function_main:
  
  
  1 = m[fp + 2] + 1
  m[fp + 6] = inverse(m[fp + 2])
  m[fp + 7] = m[fp + 2] x m[fp + 6]
  1 = m[fp + 8] + m[fp + 7]
  0 = m[fp + 8] x m[fp + 2]
  jump_if_not_zero m[fp + 7] to @if_0
  jump @else_0

@if_0:
  jump @if_else_end_0

@else_0:
  
  1 = m[fp + 3] + 0
  m[fp + 9] = inverse(m[fp + 3])
  m[fp + 10] = m[fp + 3] x m[fp + 9]
  1 = m[fp + 11] + m[fp + 10]
  0 = m[fp + 11] x m[fp + 3]
  jump_if_not_zero m[fp + 10] to @if_1
  jump @else_1

@if_else_end_0:
  
  m[fp + 5] = 300 + 0
  jump @inline_epilogue_0

@if_1:
  jump @if_else_end_1

@else_1:
  
  m[fp + 5] = 100 + 0
  jump @inline_epilogue_0

@if_else_end_1:
  
  1 = m[fp + 4] + 1
  m[fp + 12] = inverse(m[fp + 4])
  m[fp + 13] = m[fp + 4] x m[fp + 12]
  1 = m[fp + 14] + m[fp + 13]
  0 = m[fp + 14] x m[fp + 4]
  jump_if_not_zero m[fp + 13] to @if_2
  jump @else_2

@if_2:
  jump @if_else_end_2

@else_2:
  
  m[fp + 5] = 200 + 0
  jump @inline_epilogue_0

@if_else_end_2:
  jump @if_else_end_0

@inline_epilogue_0:
  
  print print: m[fp + 5]
  
  m[fp + 15] = 0 + 0
  jump @end_program with fp = m[fp + 15]

Memory size per function:
main: 16

Function Locations: 

main: 2
doesnt_work: 8


Compiled Program:

hint: label: @function_main
hint: source line number: 3
hint: source line number: 9
   0: 1 = 1 + m[fp + 2]
hint: m[fp + 6] = inverse(m[fp + 2])
   1: m[fp + 7] = m[fp + 2] x m[fp + 6]
   2: 1 = m[fp + 8] + m[fp + 7]
   3: 0 = m[fp + 8] x m[fp + 2]
   4: if m[fp + 7] != 0 jump to @if_0 = 7 with next(fp) = fp
   5: if 1 != 0 jump to @else_0 = 8 with next(fp) = fp
hint: label: @end_program
   6: if 1 != 0 jump to @end_program = 6 with next(fp) = fp
hint: label: @if_0
   7: if 1 != 0 jump to @if_else_end_0 = 14 with next(fp) = fp
hint: label: @else_0
hint: source line number: 10
   8: 1 = 0 + m[fp + 3]
hint: m[fp + 9] = inverse(m[fp + 3])
   9: m[fp + 10] = m[fp + 3] x m[fp + 9]
  10: 1 = m[fp + 11] + m[fp + 10]
  11: 0 = m[fp + 11] x m[fp + 3]
  12: if m[fp + 10] != 0 jump to @if_1 = 16 with next(fp) = fp
  13: if 1 != 0 jump to @else_1 = 17 with next(fp) = fp
hint: label: @if_else_end_0
hint: source line number: 17
  14: 300 = 0 + m[fp + 5]
  15: if 1 != 0 jump to @inline_epilogue_0 = 29 with next(fp) = fp
hint: label: @if_1
  16: if 1 != 0 jump to @if_else_end_1 = 19 with next(fp) = fp
hint: label: @else_1
hint: source line number: 11
  17: 100 = 0 + m[fp + 5]
  18: if 1 != 0 jump to @inline_epilogue_0 = 29 with next(fp) = fp
hint: label: @if_else_end_1
hint: source line number: 13
  19: 1 = 1 + m[fp + 4]
hint: m[fp + 12] = inverse(m[fp + 4])
  20: m[fp + 13] = m[fp + 4] x m[fp + 12]
  21: 1 = m[fp + 14] + m[fp + 13]
  22: 0 = m[fp + 14] x m[fp + 4]
  23: if m[fp + 13] != 0 jump to @if_2 = 25 with next(fp) = fp
  24: if 1 != 0 jump to @else_2 = 26 with next(fp) = fp
hint: label: @if_2
  25: if 1 != 0 jump to @if_else_end_2 = 28 with next(fp) = fp
hint: label: @else_2
hint: source line number: 14
  26: 200 = 0 + m[fp + 5]
  27: if 1 != 0 jump to @inline_epilogue_0 = 29 with next(fp) = fp
hint: label: @if_else_end_2
  28: if 1 != 0 jump to @if_else_end_0 = 14 with next(fp) = fp
hint: label: @inline_epilogue_0
hint: source line number: 4
hint: print(m[fp + 5]) for "print"
hint: source line number: 5
  29: 0 = 0 + m[fp + 15]
  30: if 1 != 0 jump to @end_program = 6 with next(fp) = m[fp + 15]

╔═════════════════════════════════════════════════════════════════════════╗
║                                STD-OUT                                  ║
╚═════════════════════════════════════════════════════════════════════════╝

"print" -> 200
──────────────────────────────────────────────────────────────────────────

╔═════════════════════════════════════════════════════════════════════════╗
║                                 STATS                                   ║
╚═════════════════════════════════════════════════════════════════════════╝

CYCLES: 22
MEMORY: 81

Bytecode size: 31
Public input size: 0
Private input size: 0
Runtime memory: 33 (0.00% vec) (no vec mem: 0)
Memory usage: 90.9%

──────────────────────────────────────────────────────────────────────────

test test_doesnt_work ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 21 filtered out; finished in 0.00s

[divya@archdivya leanMultisig]$

TomWambsgans

Thanks! I have added 2 comments on the code. Also, some tests do not pass (for instance test_match). But I believe this goes in the right direction.

TomWambsgans · 2025-10-16T18:37:14Z

crates/lean_compiler/src/b_compile_intermediate.rs

+                    updated_fp: None,
+                });
+
+                let remaining =


After a GOTO intuitively there should not remain any lines to compile? So we could simply assert lines[i + 1..].is_empty() instead of compiling it? Or maybe am I missing some case?

I think one cannot assert that lines[i + 1..] is empty after a GOTO. There are valid cases where lines exist after a GOTO, and those lines need to be compiled and registered with the epilogue label.

TomWambsgans · 2025-10-16T18:43:17Z

crates/lean_compiler/src/a_simplify_lang.rs

                        .zip(&simplified_args)
                        .map(|((var, _), expr)| (var.clone(), expr.clone()))
                        .collect::<BTreeMap<_, _>>();
+                    let epilogue_label = format!("@inline_epilogue_{}", total_inlined_counter.0);


This idea of "epilogue_label" looks promising. Currently you always put an epilogue_label when inlining but in some cases, when there is no instructions after the RETURN this is unnecessary (we can call such RETURNs "final"). But detecting it is not trivial. We would somehow need to peek at the following of the code (what comes after the RETURN), to see if it's terminal or not, if that makes sense

I agree, you don't need to always put the label. But yeah finding where you don't need to is quite difficult. We'll need to have some context of what is final in the remainder of the scope.

divyaranjan1905 added 2 commits October 16, 2025 09:25

add SimpleLine::Goto and refactor the inlining mechanism for it

affc160

add Line::Goto and process SimpleLine::Goto during intermediate compi…

4af51f1

…lation Also uncomments the inline_bug_mre test

TomWambsgans and others added 2 commits October 16, 2025 20:17

fmt

cdb9346

chore: typo

8cfefb2

TomWambsgans reviewed Oct 16, 2025

View reviewed changes

TomWambsgans force-pushed the main branch from 9740f2c to 182d63e Compare October 18, 2025 14:40

TomWambsgans force-pushed the main branch from c7ae238 to 04a0761 Compare October 30, 2025 20:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Fix: Check non-exhaustible conditional returns using a `goto` mechanism #75

Fix: Check non-exhaustible conditional returns using a `goto` mechanism #75

Uh oh!

divyaranjan1905 commented Oct 16, 2025 •

edited

Loading

Uh oh!

divyaranjan1905 commented Oct 16, 2025

Uh oh!

TomWambsgans left a comment

Uh oh!

TomWambsgans Oct 16, 2025

Uh oh!

divyaranjan1905 Oct 16, 2025

Uh oh!

TomWambsgans Oct 16, 2025

Uh oh!

divyaranjan1905 Oct 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Fix: Check non-exhaustible conditional returns using a goto mechanism #75

Are you sure you want to change the base?

Fix: Check non-exhaustible conditional returns using a goto mechanism #75

Uh oh!

Conversation

divyaranjan1905 commented Oct 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

divyaranjan1905 commented Oct 16, 2025

Uh oh!

TomWambsgans left a comment

Choose a reason for hiding this comment

Uh oh!

TomWambsgans Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

divyaranjan1905 Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

TomWambsgans Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

divyaranjan1905 Oct 16, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Fix: Check non-exhaustible conditional returns using a `goto` mechanism #75

Fix: Check non-exhaustible conditional returns using a `goto` mechanism #75

divyaranjan1905 commented Oct 16, 2025 •

edited

Loading