Skip to content

Instantly share code, notes, and snippets.

@jkbbwr
Created April 3, 2018 01:40
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jkbbwr/fa3b7c6ac53a57c8bcf2b2cb753e4f4a to your computer and use it in GitHub Desktop.
Save jkbbwr/fa3b7c6ac53a57c8bcf2b2cb753e4f4a to your computer and use it in GitHub Desktop.
; 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" }
@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