A builtin has the name and the options of a tool of the shell, so it must do what that tool does. TLA+ models write the cases, and the real tools give the answers. Then the pipes, the quotes and the redirections of an envelope learned to work as in a shell.
grep, sed, sort, uniq, xargs and jq, checked against the shell
Six more builtins: grep, sed, sort, uniq, xargs and jq. A builtin has the name and the options of a tool of the shell, so it must do what that tool does. "Almost the same" is a trap: you copy a command from a terminal into an envelope, and it gives a different line. Thus I did not write tests from my memory of these tools. TLC writes the cases, and the real tools give the answers.
TLC writes the cases
Each builtin has a TLA+ model, specs/ShellNAME.tla: what the tool does, from its source. For sed, the model follows match_address_p and do_subst of execute.c. For grep -w, it follows EGexecute. For jq, it follows the order in which jq 1.7 gives its outputs.
A state of a model is one case: a command, an input and the output of the model. TLC checks the invariants and writes all the states to a file. Then scripts/builtins.sh gives each case to the tool of the shell and to the builtin. The three outputs must be the same.
| Model | Cases |
|---|---|
ShellSort | 26,316 |
ShellUniq | 11,466 |
ShellGrep | 26,558 |
ShellSed | 15,222 |
ShellXargs | 15,159 |
ShellJQ | 41,897 |
The first version put the output in Init. TLC computes Init on one core, and the run took a long time. Now Init picks a case with an empty output, and Next computes it, so all the workers of TLC share the work. All six models take about 5 minutes. The CI runs them with the same versions of the tools: GNU coreutils 9.4, grep 3.11, sed 4.9, findutils 4.9.0 and jq 1.7.
The longest match
PCRE gives the first match in the order of the pattern. POSIX gives the longest one at the leftmost position. For a|ab and the text ab, PCRE gives a, and grep -o gives ab. For a pattern with no | and no repeat of a group, the first match of PCRE is also the longest one: a check of 25,344 patterns and 62 texts found no difference. For the other patterns, FIFO.Builtin.Regex has an NFA.
My first NFA gave each step to :re.run, with the text and an offset. It was slow on a long line: sed -E 's/(a|b)+/X/g' on 300 KB took 17 seconds. :re.run checks the UTF-8 of all the text after the offset at each call, about 300 µs for 300 KB, so many matches on one line cost the square of its length. Now :re.run gets one character for an atom, and the characters before and after a position for ^ or \b. PCRE still finds the start of each match fast, and the NFA runs only from that start. When PCRE has read the text 4 times, the NFA searches alone. The same sed now takes about 0.6 seconds.
The NFA also changed a limit. (a+)+$ on 40 a and a c was an error before: PCRE tries too many paths. The NFA walks each character one time, so sed now gives the correct output, and grep tries the NFA when PCRE gives up.
A budget for the work
Each character costs the NFA at most its number of states. My first budget was 1,000,000 steps for one line. Then I saw the problem: a pattern with many states, on many short lines, stays under the budget on each line, and the input has 1 MiB of lines. Now a run of grep or sed has 5,000,000 steps for all its lines, and the steps of grep, sed and jq also count in the work of the Request: 10,000,000 in all. A Request runs at most 1024 builtins, so a budget only for one run was not sufficient.
The count also missed work at first: (a?){300}b on 5000 characters took 15 seconds before the error, because the steps did not count the closures of the states. Now the states of one character share one walk, each state that it reaches is a step, and the same pattern stops after about 2 seconds.
What a random comparison found
The models cover small inputs, so I also compared the builtins with GNU on random patterns: more than 20,000 cases of grep -o, -ow and -ox, and 30,000 cases of sed s. Each difference went into a model or into a test, and the models still agree with the tools.
- **
grep -o -wafter the first match.** To try a shorter match,EGexecutegivesre_matchthe lengthmatch + len - ptr. That is the length from the start of the line minus the start of the search. At the first search of a line the two are equal. After a match, a shorter match must end that many bytes earlier. Thus GNU givesafora.a.bwithgrep -ow 'a\.*', and my builtin gaveatwo times. The builtin now has the same loop, and the model too. - **The groups of
\{m,n\}.**s/\(a*\)\{0,2\}b/[\1]/onaabgives[]in GNU, not[aa]. glibc buildsx{0,2}as(x? x)?, so two repeats use the second copy last. Only the first optional copy is marked as optional, becausecreate_token_treeclears that mark in each copy. Andupdate_regsputs back the groups of the last part that was not empty only for an optional copy. I compiled the regex code of gnulib with traces to see this. The NFA now has the shape of the tree of glibc and walks it asset_regsdoes, andShellSedhas the same rule for intervals. - **
^^in a BRE** is the anchor and the character^. - **
xargs echo -e**: the options of GNU xargs end at the command, so-egoes toecho. Mine read it as an option ofxargs.
I did not copy two things of glibc. grep -o 'a*\(a\|b \)\>' finds b in a b , but \> cannot match after a space, and the same pattern with no a* does not find it. And with \b between two parts that can take the same characters, glibc gives the characters to the second part. The match is the same; only the groups change. To copy this, I would need the DFA of glibc.
jq 1.7, not the jq that I remembered
Ubuntu 24.04 has jq 1.7.1. The CI installs the release binary of jq 1.7, and my first runs used 1.7.1, so I compared with the binary of the CI too. Most differences were not between these two versions: my error messages came from a newer jq. [] | .a gives Cannot index array with string "a" in jq 1.7, and 1 % 0 says "divided (remainder)". A filter can catch such a message with try ... catch ., so it must be the same text. The functions that jq 1.7 writes in jq (src/builtin.jq, for example join, sub and reverse) now have the same text in the builtin, so they give the same outputs and errors: "abc" | reverse is an error in jq 1.7.
Numbers were the largest surprise. jq 1.7 keeps the text of a number of the input while no operation changes it, in the form of decNumber: {"price": 1.50} | .price gives 1.50, 1.0 stays 1.0, 3e2 becomes 3E+2, and 100000000000000000001 keeps all its digits. Mine gave 1.5, 1 and 300. The JSON module of OTP already gives the text of each number to its callbacks, so the builtin keeps it there, and arithmetic uses the float. Two such numbers compare as decimals: 1.000000000000000000001 == 1 is false.
The grammar also had two traps. as $x belongs to a term, so .a + 1 as $x | $x is .a + (1 as $x | $x); my parser refused it. And -. or -1 is a filter, not an option: jq takes a word as an option only when a letter or a - comes after its -. The value of an object pair is smaller than a filter in jq 1.7, so {a: 1 + 1} is an error there, and now here too.
ShellJQ now has numbers with their text, and it found no difference after these changes.
Smaller fixes
- The coverage of the tests found that
grep -Fdropped the bytes that are not UTF-8 from its pattern. sed 's/a/\xff/'puts a byte that is not UTF-8 into a line. The next command still matched by characters, and the match raised an exception. Now each line selects its matcher.- The output of each builtin, but
cat, now has no line breaks at its end, as$( )of a shell. Before, onlyhead,tailandcutremoved the last one.xargskeeps them between its runs, as a pipe of a shell does.
Pipes, as in a shell
In a shell, printf 'a\n' | wc -l gives 1. In an envelope of mkfifo.com, it gave 0. Each value between two commands lost the line breaks at its end, so wc -l did not see the line break of printf. A script of sh gave 1, because the shell keeps the bytes of each command. Thus the same command gave two different numbers, in two places of the same site.
Now an envelope does what a shell does. A pipe gives the bytes of a command to the next command, with the line breaks at their end. Only the value has no line breaks at its end: the value of $( ), and the text that a pipe puts in the envelope, as $( ) of a shell gives it.
# The body: {"items": [1, 2, 3]}
$body | jq '.items[]' | wc -lBefore, this gave 2: jq writes 1, 2 and 3 on three lines, but the pipe removed the last line break, and wc counts the line breaks. Now it gives 3, as in a terminal.
How
The function that runs a command gets one more argument: does its output go to a pipe? FIFO.Template gives "yes" to each command before a |, and "no" to the last one. A builtin then gives the bytes of its tool, or its value with no line breaks at its end. The answer of a FIFO in a pipe is the same: the next command gets its body as it is.
The shell asks for "yes" for the last command too, because a script writes its output as it is. Thus the shell and the envelopes now use the same code for a pipe. The shell had its own code for it before, and that was why the two did not agree.
cat gives its input with no change in all places, because it gives the bytes of a file, as the fonts of this site.
The home is ~
A script of sh and eval, and each builtin of /bin, runs with a home that is not a FIFO, so that totp gives no code of a FIFO there, and hmac opens no sealed key of a FIFO. That home was @sh. Now it is ~, the home of a shell. The name of a FIFO has only a to z, 0 to 9, -, _ and ., so no FIFO has ~ in its name, and the home stays a home of no FIFO.
Backslashes in double quotes
In a shell, a backslash in double quotes keeps the next character only before $, ` `, " and a second backslash. Before a different character, the backslash stays. Thus "a\\b" is a\b, and "a\b" is a\b` too.
The words of the FIFO syntax had only two of these escapes: \" and \$. So "a\\b" stayed a\\b. That looks small, but it changed commands that you copy from a terminal:
$body | sed "s/\\./,/g"In a shell, sed gets s/\./,/g and changes each dot. Here, sed got s/\\./,/g: a backslash, then any character. Now the words of an envelope, of sh and of the terminal have the four escapes of a shell, and this command does the same thing in all of them.
The shell of mkfifo.com finds the end of each command before it reads the words. Its splitter has the same rule now, so both agree on where a text in double quotes ends: in "a\\" b, the quote ends after a\. set also writes \ and ` `` with a backslash in double quotes, so that each line that it shows gives the same value when you run it again.
Redirections: a FIFO is a named pipe
On Unix, mkfifo my_pipe makes a named pipe, and a command writes into it with >, as into a file. mkfifo.com has its name from that pipe, but its syntax had no < and no >. The shell and the terminal gave an error for each redirection, so that a command from a terminal did not do a different thing here with no word about it. Now they work, in the envelopes, in sh and in the terminal:
$(wc -l < prices) # the answer of a GET of the FIFO prices
$(printf '%s\n' $id > audit) # a Request to audit, with no output
$($body | jq -r .id 2>/dev/null) # empty when jq fails
$(jq .id 2>&1) # the error as the valueWhat each one does
> fifosends the output to the FIFO as the body of a Request, asteedoes, and the command gives no output. A FIFO keeps nothing that a second write could replace, so>>does the same as>.< fifogives the command the answer of aGETof the FIFO. Only an envelope with a lineX-HTTP-Method-Overrideagrees with aGET, so a FIFO tells which envelopes a reader can read.2> fifosends the error to the FIFO, asErrors-Todoes for an egress envelope.2>&1makes the error the output./dev/nulltakes the output and the error, and gives an empty input. It sends no Request.
They act from the left to the right, as in a shell. In > log 2>&1, the error goes to log. In 2>&1 > log, the error goes where the output was at that time: into the value.
An error that moves does not stop the line
In an envelope, a command that fails stops the egress. There is no || to go on after it. Now 2>/dev/null is the way: an error that a redirection moves to a FIFO, to /dev/null or to the value is not a failure. An error of the redirection itself, for example a FIFO with no ingress envelope, still stops the line.
Names in the text
A target is the name of a FIFO, with no variable. Thus the graph knows each FIFO that an envelope reads or writes, as it knows the FIFOs of tee, and the save refuses a loop: an envelope of ping with > pong, and an envelope of pong with < ping, get 422.
< and > in a word
In a shell, < and > out of quotes end a word: printf a>log writes a into log. The words of an envelope do the same now. One thing changed with it: out of $( ), the words of a pipe go to the end of the line, so <td>$x | tr a-z A-Z</td> reads a FIFO /td, and the save refuses it. The pipe goes in $( ): <td>$($x | tr a-z A-Z)</td>. A sealed word, <seal:KEY>, stays a word.
The function that runs a command
A pipe gives the function that runs a command a name, its words, its input, and the flag for the line breaks at the end of its output. The redirections use the same function, with two more names: {:read, fifo} for <, and {:write, fifo} for >. For an envelope, these are FIFO.read/2, a new GET with the hops and the messages of the Request, and FIFO.send/3, which tee uses. For the terminal, they give an error, as a pipe to a FIFO does: the terminal sends nothing. /dev/null never goes to the function.