src/rules/suspicious/fuel.bend checks

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

rule fuel: a call to a def of the same file, its name then (, passes a Nat literal (1000n: digits, then n) where that def takes its fuel. 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 literal comes out cut short, with no error (a JSON printer that stopped at 1000 tasks). Inside a law, the checker unrolls the fixed fuel and hangs. Derive the fuel from the input's size (Nat.mul(size, 4n)) or take it as a parameter. A literal of any size counts, an exact repeat count such as 3n included. Only an argument that is one literal token alone counts: U32.to_nat(1000), 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 24 · 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 28 · raw

@+nn:String -> Bool

is it a fuel parameter's name?

def fuels.params source · line 33 · raw

@ps:List<&2, 0x013e0f9a479bbebad5ed196725eede95/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 42 · raw

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

every fuel parameter of every def of the file

def literal source · line 50 · raw

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

an argument that is a Nat literal alone (digits, then n), as a finding

def call source · line 61 · raw

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

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

def calls source · line 71 · raw

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

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

def own source · line 89 · raw

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

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

def check.go source · line 97 · raw

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

each top-level statement, walked as its own def

def check source · line 108 · raw

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

the rule