-
-
Save jkbbwr/fa3b7c6ac53a57c8bcf2b2cb753e4f4a to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
; ModuleID = 'bitcode.bc' | |
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128" | |
target triple = "x86_64-unknown-linux-gnu" | |
%struct.ObjHeader = type { %struct.TypeInfo*, i32 } | |
%struct.TypeInfo = type { %struct.GlobalHash, i32, %struct.TypeInfo*, i32*, i32, %struct.TypeInfo**, i32, %struct.MethodTableRecord*, i32, %struct.FieldTableRecord*, i32, %struct.ObjHeader*, %struct.ObjHeader* } | |
%struct.GlobalHash = type { [20 x i8] } | |
%struct.MethodTableRecord = type { i64, i8* } | |
%struct.FieldTableRecord = type { i64, i32 } | |
%struct.InitNode = type { void (i32)*, %struct.InitNode* } | |
@"kobj:kotlin.Unit" = external global %struct.ObjHeader | |
; Function Attrs: nounwind uwtable | |
declare %struct.ObjHeader* @AllocInstance(%struct.TypeInfo*, %struct.ObjHeader**) #0 | |
; Function Attrs: nounwind uwtable | |
declare %struct.ObjHeader* @AllocArrayInstance(%struct.TypeInfo*, i32, %struct.ObjHeader**) #0 | |
; Function Attrs: uwtable | |
declare %struct.ObjHeader* @InitInstance(%struct.ObjHeader**, %struct.TypeInfo*, void (%struct.ObjHeader*)*, %struct.ObjHeader**) #1 | |
; Function Attrs: nounwind uwtable | |
declare void @UpdateReturnRef(%struct.ObjHeader**, %struct.ObjHeader*) #0 | |
; Function Attrs: nounwind uwtable | |
declare void @UpdateRef(%struct.ObjHeader**, %struct.ObjHeader*) #0 | |
; Function Attrs: norecurse nounwind readnone uwtable | |
declare void @EnterFrame(%struct.ObjHeader**, i32, i32) #2 | |
; Function Attrs: nounwind uwtable | |
declare void @LeaveFrame(%struct.ObjHeader**, i32, i32) #0 | |
; Function Attrs: norecurse nounwind readnone uwtable | |
declare %struct.ObjHeader** @GetReturnSlotIfArena(%struct.ObjHeader**, %struct.ObjHeader**) #2 | |
; Function Attrs: norecurse nounwind readonly uwtable | |
declare %struct.ObjHeader** @GetParamSlotIfArena(%struct.ObjHeader*, %struct.ObjHeader**) #3 | |
; Function Attrs: nounwind readnone uwtable | |
declare i8* @LookupOpenMethod(%struct.TypeInfo*, i64) #4 | |
; Function Attrs: nounwind readonly uwtable | |
declare i8 @IsInstance(%struct.ObjHeader*, %struct.TypeInfo*) #5 | |
; Function Attrs: uwtable | |
declare void @CheckInstance(%struct.ObjHeader*, %struct.TypeInfo*) #1 | |
; Function Attrs: noreturn uwtable | |
declare void @ThrowException(%struct.ObjHeader*) #6 | |
; Function Attrs: norecurse nounwind uwtable | |
declare void @AppendToInitializersTail(%struct.InitNode*) #7 | |
; Function Attrs: uwtable | |
declare void @Kotlin_initRuntimeIfNeeded() #1 | |
; Function Attrs: nounwind | |
declare i32 @__gxx_personality_v0(...) #8 | |
; Function Attrs: nounwind | |
declare i8* @__cxa_begin_catch(i8*) #8 | |
; Function Attrs: nounwind | |
declare void @__cxa_end_catch() #8 | |
; Function Attrs: argmemonly nounwind | |
declare void @llvm.memset.p0i8.i32(i8* nocapture, i8, i32, i32, i1) #9 | |
declare void @__VERIFIER_error() #10 | |
declare void @__VERIFIER_assume(i32) #10 | |
declare i32 @nd() #10 | |
define void @"main"(%struct.ObjHeader*) #10 personality i8* bitcast (i32 (...)* @__gxx_personality_v0 to i8*) { | |
prologue: | |
%k = alloca i32 | |
%j = alloca i32 | |
%1 = alloca %struct.ObjHeader*, i32 2 | |
%2 = bitcast %struct.ObjHeader** %1 to i8* | |
call void @llvm.memset.p0i8.i32(i8* %2, i8 0, i32 16, i32 8, i1 false) | |
call void @EnterFrame(%struct.ObjHeader** %1, i32 1, i32 2) | |
br label %locals_init | |
locals_init: ; preds = %prologue | |
%3 = phi %struct.ObjHeader** [ %1, %prologue ] | |
%4 = ptrtoint %struct.ObjHeader** %3 to i64 | |
%5 = or i64 %4, 1 | |
%6 = inttoptr i64 %5 to %struct.ObjHeader** | |
%p-args = getelementptr %struct.ObjHeader*, %struct.ObjHeader** %3, i32 1 | |
store %struct.ObjHeader* %0, %struct.ObjHeader** %p-args | |
br label %entry | |
entry: ; preds = %locals_init | |
%7 = invoke i32 @nd() | |
to label %call_success unwind label %cleanup_landingpad | |
call_success: ; preds = %entry | |
%8 = invoke i32 @Kotlin_Int_compareTo_Int(i32 %7, i32 0) | |
to label %call_success1 unwind label %cleanup_landingpad | |
call_success1: ; preds = %call_success | |
%9 = icmp sgt i32 %8, 0 | |
br i1 %9, label %when_case, label %when_next | |
when_case: ; preds = %call_success1 | |
br label %when_exit | |
when_next: ; preds = %call_success1 | |
br label %when_exit | |
when_exit: ; preds = %when_next, %when_case | |
%10 = phi i32 [ 1, %when_case ], [ 0, %when_next ] | |
invoke void @__VERIFIER_assume(i32 %10) | |
to label %call_success2 unwind label %cleanup_landingpad | |
call_success2: ; preds = %when_exit | |
%11 = invoke i32 @nd() | |
to label %call_success3 unwind label %cleanup_landingpad | |
call_success3: ; preds = %call_success2 | |
store i32 %11, i32* %k | |
%12 = load i32, i32* %k | |
%13 = invoke i32 @Kotlin_Int_compareTo_Int(i32 %12, i32 %7) | |
to label %call_success7 unwind label %cleanup_landingpad | |
call_success7: ; preds = %call_success3 | |
%14 = icmp sgt i32 %13, 0 | |
br i1 %14, label %when_case6, label %when_next5 | |
when_case6: ; preds = %call_success7 | |
br label %when_exit4 | |
when_next5: ; preds = %call_success7 | |
br label %when_exit4 | |
when_exit4: ; preds = %when_next5, %when_case6 | |
%15 = phi i32 [ 1, %when_case6 ], [ 0, %when_next5 ] | |
invoke void @__VERIFIER_assume(i32 %15) | |
to label %call_success8 unwind label %cleanup_landingpad | |
call_success8: ; preds = %when_exit4 | |
store i32 0, i32* %j | |
br label %loop_check | |
while_loop: ; preds = %call_success9 | |
%16 = load i32, i32* %j | |
%17 = invoke i32 @Kotlin_Int_inc(i32 %16) | |
to label %call_success10 unwind label %cleanup_landingpad | |
call_success10: ; preds = %while_loop | |
store i32 %17, i32* %j | |
%18 = load i32, i32* %k | |
%19 = invoke i32 @Kotlin_Int_dec(i32 %18) | |
to label %call_success11 unwind label %cleanup_landingpad | |
call_success11: ; preds = %call_success10 | |
store i32 %19, i32* %k | |
br label %loop_check | |
loop_check: ; preds = %call_success11, %call_success8 | |
%20 = load i32, i32* %j | |
%21 = invoke i32 @Kotlin_Int_compareTo_Int(i32 %20, i32 %7) | |
to label %call_success9 unwind label %cleanup_landingpad | |
call_success9: ; preds = %loop_check | |
%22 = icmp slt i32 %21, 0 | |
br i1 %22, label %while_loop, label %loop_exit | |
loop_exit: ; preds = %call_success9 | |
%23 = load i32, i32* %k | |
%24 = invoke i32 @Kotlin_Int_compareTo_Int(i32 %23, i32 0) | |
to label %call_success14 unwind label %cleanup_landingpad | |
call_success14: ; preds = %loop_exit | |
%25 = icmp slt i32 %24, 0 | |
br i1 %25, label %when_case13, label %when_exit12 | |
when_case13: ; preds = %call_success14 | |
invoke void @__VERIFIER_error() | |
to label %call_success15 unwind label %cleanup_landingpad | |
call_success15: ; preds = %when_case13 | |
br label %when_exit12 | |
when_exit12: ; preds = %call_success15, %call_success14 | |
br label %epilogue | |
unreachable: ; No predecessors! | |
br label %epilogue | |
epilogue: ; preds = %unreachable, %when_exit12 | |
call void @LeaveFrame(%struct.ObjHeader** %3, i32 1, i32 2) | |
ret void | |
cleanup_landingpad: ; preds = %when_case13, %loop_exit, %loop_check, %call_success10, %while_loop, %when_exit4, %call_success3, %call_success2, %when_exit, %call_success, %entry | |
%26 = landingpad { i8*, i32 } | |
cleanup | |
call void @LeaveFrame(%struct.ObjHeader** %3, i32 1, i32 2) | |
resume { i8*, i32 } %26 | |
} | |
declare i32 @Kotlin_Int_compareTo_Int(i32, i32) | |
declare i32 @Kotlin_Int_inc(i32) | |
declare i32 @Kotlin_Int_dec(i32) | |
attributes #0 = { nounwind uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #1 = { uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #2 = { norecurse nounwind readnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #3 = { norecurse nounwind readonly uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #4 = { nounwind readnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #5 = { nounwind readonly uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #6 = { noreturn uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #7 = { norecurse nounwind uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="false" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } | |
attributes #8 = { nounwind } | |
attributes #9 = { argmemonly nounwind } | |
attributes #10 = { "no-frame-pointer-elim"="true" } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
@SymbolName("__VERIFIER_error") | |
external fun __VERIFIER_error() | |
@SymbolName("__VERIFIER_assume") | |
external fun __VERIFIER_assume(p0: Int) | |
@SymbolName("nd") | |
external fun nd(): Int | |
fun main(args: Array<String>) { | |
val n = nd() | |
__VERIFIER_assume(if (n > 0) 1 else 0) | |
var k = nd() | |
__VERIFIER_assume(if (k > n) 1 else 0) | |
var j = 0; | |
while (j < n) { | |
j++ | |
k-- | |
} | |
if (k < 0) { | |
__VERIFIER_error() | |
} | |
return | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment