cint university / 201 / ced, the cint editor
201-06: the workbench
This is lesson 201-06 of CU-201.2, checked against cint 0.2.0.
You will open a session on a module and ask it questions. Then you will run a year of interest in one command. You will find the first day the balance reached 1040.00 and walk through the operations of an entry that faulted.
This lesson needs cint on your own computer, with the debugging tools from setup.
the module
Save this as savings.ci:
// savings.ci: a savings balance in cents, with interest paid daily.
export I64 balance = 100_000; // 1000.00
I64 daily_interest(I64 cents, I64 basis_points) {
return muldiv(I64, cents, basis_points, 10_000 * 365, half_even);
}
// One day: add a day's interest at a yearly rate in basis points.
export void day(I64 basis_points) {
balance += daily_interest(balance, basis_points);
}
Every cint file is a module. This one has no main, so it does nothing on its own: other code uses what it exports. balance and day are exported; daily_interest is not. A basis point is a hundredth of a percent, so 450 basis points is 4.50 percent a year.
open a session
In VS Code, open the folder that holds savings.ci and choose Terminal > New Terminal. Any other terminal in that folder works the same way. Type:
$ cint workbench savings.ci
cint workbench profile cint-core-1 backend cpu-sir-interp new session
loaded savings (savings.ci)
ci[2]>
cint repl opens the same session. The first line says where entries run: cpu-sir-interp is the interpreter. The prompt counts entries, the things you type that run; loading the module was entry 1.
ask it questions
Type an expression and the workbench answers with its exact value and its type:
ci[2]> savings.balance
= 100000 : I64
ci[3]> :inspect savings.balance /scale 100
savings.balance : I64 shown with scale 100
exact 1000.0
raw 100000
ci[3]> savings.daily_interest(1, 2)
error[C3008]: undefined or unusable name
--> entry 3:1:9
|
1 | savings.daily_interest(1, 2)
| ^
|
ci[4]>
- A name from the module is written with the module's name in front:
savings.balance. - A line that starts with a colon is a command. Commands are not entries, so the count stays at 3.
:inspectshows a value in other forms./scale 100divides it by 100, so cents read as dollars, and/alladds hexadecimal, binary and the bytes in memory. - The session sees only what the module exports.
daily_interestis not exported, so the third entry is an error, and an entry with an error still counts. A position inside an entry readsentry 3:1:9: entry 3, line 1, character 9.
run a year
A statement changes the module's state. Save the state first, then pay one day of interest:
ci[4]> :checkpoint start
checkpoint start #1 revisions: savings@r1
ci[4]> savings.day(450);
ci[5]> savings.balance
= 100012 : I64
A checkpoint is a saved copy of the state, under a name you choose, and #1 is its number. savings@r1 names the revision of the module it holds. Each time a module's code changes in a session, its revision number goes up. One day at 4.50 percent adds 12 cents.
To run the other 364 days, declare a function in the session and run it with :run:
ci[6]> export void d() { savings.day(450); }
d : () -> void revision session@r1
ci[7]> :run d() 364
ci[371]> savings.balance
= 104629 : I64
ci[372]> :checkpoint year
checkpoint year #2 revisions: session@r1, savings@r1
:run calls an exported function of the session, here d, as many times as you say, and each call is one entry. The session's own code has revisions too, so d is session@r1. The year ends at 1046.29. Day 1 was entry 4, and days 2 to 365 are entries 7 to 370, so from day 2 on, the entry number is 5 more than the day.
compare two states
:diff compares the current state with a checkpoint, one name at a time:
ci[372]> :diff start
binding status differing first canonical difference
savings.balance differs 1 104629 here, 100000 in start
A binding is a name with its value. Only balance changed.
find the first day
To find the day the balance first reached 1040.00, run :replay with --when:
ci[372]> :replay start --when savings.balance >= 104_000
savings.balance >= 104_000 first holds at entry 322
bisection: 11 probes over 367 boundaries; PRED is taken as monotone
Entry 322 is day 317. A boundary is the point after an entry, where the workbench can compare or test the state, and there are 367 of them since start. The workbench did not test the condition at every one. It replayed from the checkpoint to the middle, tested there and halved the range, 11 probes in all. This is called bisection. It works only when the condition stays true once it holds. That is what PRED is taken as monotone means. Here it does, because the balance only grows. For a condition that can turn false again, the answer may not be the first entry where it holds.
a fault in the session
Put the balance near the largest I64 and pay a day of interest:
ci[372]> savings.balance = I64.max - 100;
ci[373]> savings.day(450);
fault[E_OVERFLOW]: the exact result is outside the type's range
--> savings.ci:11:13
|
11 | balance += daily_interest(balance, basis_points);
| ^ add.checked.i64
|
= operation: add.checked.i64
= operand-count: 2
= operand: I64 9223372036854775707
= operand: I64 1137128059338260
= exact: 9224509164914113967
= limit: I64 9223372036854775807
= revision: 03b315aa3c24f675b5fd489839960d132c9a000f478a1cb8310eee016fb5609f
= source-map: none
= address: none
= stack-depth: 1
= called from: entry 373:1:9
= fuel-consumed: 3 (not part of the fault record)
= state: no store completed in this entry; context reset
= noncanonical: not part of the fault record
= stack-source: entry 373:1:9
|
1 | savings.day(450);
| ^
|
= workbench-position: entry 373
= site: day#5
= backend: cpu-sir-interp
ci[374]> savings.balance
= 9223372036854775707 : I64
This is the layout that cint run prints. The lines from operation to stack-depth are the fault record, and every way of running the program reports the same values in them. The lines after = noncanonical are not part of the record. They say where the workbench found the fault: the source of each call, the entry, the operation's place in day and where the entry ran.
The interest was computed, but adding it to the balance went past the limit. no store completed in this entry means the entry changed nothing: balance still holds the value from before it. context reset means the session cleared the fault so that the next entry can run.
:trace replays an entry and lists every counted operation it made, in order. :trace fault picks the last entry that faulted:
ci[375]> :trace fault
entry 373 savings.day(450); evaluator cpu-sir-interp, by replay
ord position operation operands value
0 entry 373:1:9 call 450
1 savings.ci:11:16 call 9223372036854775707, 450
2 savings.ci:6:52 mul.checked.i64 10000, 365 3650000
3 savings.ci:6:12 muldiv.checked.i64.i64.half_even 9223372036854775707, 450, 3650000 1137128059338260
- savings.ci:11:16 return 1137128059338260
4 savings.ci:11:13 add.checked.i64 9223372036854775707, 1137128059338260 E_OVERFLOW
Read it from the top: the call to day, the call to daily_interest, the multiplication 10_000 * 365, the muldiv, the return and the addition that faulted. Each row holds the operands the operation saw and the value it gave. The row marked - is the return, which is listed but not counted. Every plain operator is checked, including the multiplication 10_000 * 365.
go back
:restore makes a checkpoint the current state again:
ci[375]> :restore year
saved current state as auto-1
restored year #2
ci[375]> savings.balance
= 104629 : I64
Before it restores year, the workbench saves the current state as a checkpoint named auto-1, which you can restore in turn.
:undo goes back one entry:
ci[376]> savings.balance = 0;
ci[377]> :undo
saved current state as auto-2
back to the state before entry 376
ci[377]> savings.balance
= 104629 : I64
check the interpreter against C
The session runs entries in the interpreter. --check cpu-c17 runs each call a second time in your C compiler's build of the module and compares the two:
ci[378]> :run d() 3 --check cpu-c17
check: cpu-sir-interp and cpu-c17 agree at 3 boundaries
ci[381]> savings.balance
= 104668 : I64
After each of the 3 calls, the interpreter and the compiled C held the same state. The first --check of a module also prints a line as it builds the module with your C compiler, and later sessions reuse that build. If they ever differ, :run stops at the first call where they do. Such a difference is a defect in cint. Report it with the session.
go to any entry
:goto makes the state at the end of any entry current, by replay:
ci[382]> :goto 322
saved current state as auto-3
at the end of entry 322, reached by replay
later entries go on branch entry-322, from auto-4
ci[382]> savings.balance
= 104005 : I64
ci[383]> :goto 321
saved current state as auto-5
at the end of entry 321, reached by replay
later entries go on branch entry-321, from auto-6
ci[383]> savings.balance
= 103992 : I64
At the end of day 316 the balance was 1039.92, and at the end of day 317 it was 1040.05, which agrees with the answer of --when. Each :goto saves two checkpoints: the state you left, as auto-3, and the state it reached, as auto-4. An entry typed now starts a branch, a second line of entries from this point, and the entries of the year stay as they were. Entry numbers keep counting across branches, so the prompt still says 382. :goto fault goes to the end of the last entry that faulted.
To leave, type :quit --yes. A plain :quit warns you first, because an unsaved session is lost when it ends. A second :quit ends it. :save FOLDER keeps a session to reopen with :open FOLDER.
why it can go back
Every entry gives the same result each time it runs: the same values, the same output, the same fault at the same operation. The workbench therefore does not record what the machine did. It keeps the checkpoints and the entries typed since, and it reaches any point by replaying from the nearest checkpoint. The checks in this lesson rest on the same fact: replaying entry 373 for :trace faulted at the same operation with the same operands, and so will every replay of it.
elsewhere
In C, going back takes a debugger that records the run as it goes, such as GDB's record command, rr on Linux or Time Travel Debugging in WinDbg on Windows. GDB's checkpoint command can also save a copy of the running process to return to. Python's debugger, pdb, has no way to run backward.
walk-through
export void d() { savings.day(450); } is declared in the session, not in savings.ci. The session is a module of its own, and :run calls its exports.
10_000 * 365 turns a yearly rate into one day's interest. A rate in basis points is a share of 10,000, and a year has 365 days, so muldiv multiplies the balance by the rate and divides by both at once. It rounds a tie to even and cannot overflow in between.
I64.max - 100 is 9223372036854775707, the largest I64 less 100.
try this
- After
:run d() 364, ask:replay start --changed savings.balance, which names the last entry sincestartthat changedbalance. Which entry does it name, and why that one? - Find the first day the balance reaches 1045.00, then check it with two
:gotocommands. - Type
:restore start, declaredagain with 9000 basis points (90 percent a year) and run it 365 times. The year at 4.50 percent gained 46.29. Is the gain at 90 percent more or less than twenty times that, and why?