src/rules/suspicious/fuel.bend checks

raw source on the hub · import 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/suspicious/fuel.bend as Fuel

rule fuel: a call to a def of the same file, its name then (, passes a fixed number where that def takes its fuel: a Nat literal (1000n: digits, then n), or U32.to_nat of a U32 literal (U32.to_nat(100000): digits alone), the form a big fuel is written in. A fuel parameter is known by its name alone (its first lowercase name before the colon): fuel, gas, steps or budget, or any name starting with fuel. The fuel-0 arm returns what it has, so input past the number comes out cut short, with no error (a JSON printer that stopped at 1000 tasks). A law is no safer: a law proved over every fuel and then used at a big fixed one, against a goal written another way, overflows the checker ("the machine stack overflowed", bend 2.0.33 and 2.0.34; ez's lock walk at U32.to_nat(100000) did). Before 2.0.29 the checker unrolled the fixed fuel and hung; 2.0.29 made a checked recursion on a Nat literal linear. Derive the fuel from the input's size (Nat.mul(size, 4n)) or take it as a parameter. A number of any size counts, an exact repeat count such as 3n included. Only an argument that is the literal alone, or U32.to_nat( the U32 literal alone ), counts: a let-bound literal and a parenthesized (7n) are not seen. A def's own calls are exempt: its step passes fuel - 1, not a literal.

9 imports

import Base
import ../../src.bend as Src
import ../../lazy/lazy.bend as Lazy
import ../../finding.bend as F
import ../../syntax/lex.bend as Lex
import ../../syntax/tree.bend as Tree
import ../../syntax/bind.bend as Bind
import ../calls.bend as Calls
import ../tokens.bend as T

Types

type Fuel source · line 30 · raw

Data

a def of the file and the position of a fuel parameter

Fuel
```
@name:String -> @at:Nat -> Fuel
```

Definitions

def is_fuel source · line 34 · raw

@+nn:String -> Bool

is it a fuel parameter's name?

def fuels.params source · line 39 · raw

@ps:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node> -> @+name:String -> @+ii:Nat -> List<&2, Fuel>

the fuel parameters among a def's parameters, from position i on

def fuels source · line 48 · raw

@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/calls.Def> -> List<&2, Fuel>

every fuel parameter of every def of the file

def converted source · line 57 · raw

@kids:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @ok:Bool -> @+ll:U32 -> @+cc:U32 -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the group of a call at line ll, column cc, as a finding when it holds one U32 literal alone (digits) and ok says the call is U32.to_nat(

def literal source · line 70 · raw

@aa:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

an argument that is a Nat literal alone (digits, then n), or U32.to_nat of a U32 literal alone, as a finding

def call source · line 84 · raw

@fs:List<&2, Fuel> -> @+name:String -> @+as:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node> -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

a call to name with these arguments, against every fuel parameter

def calls source · line 94 · raw

@nn:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+fs:List<&2, Fuel> -> @+self:String -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

every call at any depth of a chain, but the def's own (self)

def own source · line 112 · raw

@mm:Maybe<&2, String> -> String

a def's (or a law's) name, "" when it has none

def check.go source · line 120 · raw

@root:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+fs:List<&2, Fuel> -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

each top-level statement, walked as its own def

def check source · line 131 · raw

@ss:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/src.Src -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the rule