diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index 60b272fcd..badc6567c 100644 --- a/src/kontrol/kdist/cheatcodes.md +++ b/src/kontrol/kdist/cheatcodes.md @@ -43,6 +43,7 @@ module FOUNDRY-CHEAT-CODES imports EVM-ABI imports FOUNDRY-ACCOUNTS imports INFINITE-GAS + imports ID configuration @@ -92,6 +93,7 @@ module FOUNDRY-CHEAT-CODES .Map + .Map ``` @@ -642,6 +644,82 @@ function toString(int256) external returns (string memory); [preserves-definedness] ``` +### `envOr(...)` cheatcodes + +The `envOr` cheatcodes in Foundry are used to read environment variables with a fallback. +In Kontrol, `envOr` is currently only implemented for concrete execution, and we always +returns the default value. + +```k + rule [envOr-word]: + #cheatcode_call SELECTOR ARGS + => #getEnvOrValue SELECTOR #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) #range(ARGS, 32, 32) + ... + + requires SELECTOR in ( + SetItem( selector ( "envOr(string,bool)" ) ) + SetItem( selector ( "envOr(string,uint256)" ) ) + SetItem( selector ( "envOr(string,int256)" ) ) + SetItem( selector ( "envOr(string,address)" ) ) + SetItem( selector ( "envOr(string,bytes32)" ) ) + ) + [preserves-definedness] + + rule [envOr-string]: + #cheatcode_call SELECTOR ARGS + => #getEnvOrValue SELECTOR #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) (Int2Bytes(32, 32, BE) +Bytes #range(ARGS, #asWord(#range(ARGS, 32, 32)), lengthBytes(ARGS) -Int #asWord(#range(ARGS, 32, 32)))) ... + //#getEnvOrValue SELECTOR #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) #enc( #tuple( #string( "default" ) ) ) ... + requires SELECTOR ==Int selector( "envOr(string,string)" ) + [preserves-definedness] + // The following rule, which is more readable, doesn't work. Needs investigation. + // #let DATA_OFFSET = #asWord(#range(ARGS, 32, 32)) #in + // #let DATA_SIZE = #asWord(#range(ARGS, DATA_OFFSET, 32)) #in + // #let DATA = #range(ARGS, 32 +Int DATA_OFFSET, DATA_SIZE) #in + // #let VARNAME = #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) #in + // #getEnvOrValue SELECTOR VARNAME DATA + + rule [envOr-bytes]: + #cheatcode_call SELECTOR ARGS + => #getEnvOrValue SELECTOR #range(ARGS, 96, #asWord(#range(ARGS, 64, 32))) #range(ARGS, #asWord(#range(ARGS, 32, 32)), 32 +Int #asWord(#range(ARGS, #asWord(#range(ARGS, 32, 32)), 32)))... + requires SELECTOR ==Int selector( "envOr(string,bytes)" ) + [preserves-definedness] + + rule [envOr-word-array]: + #cheatcode_call SELECTOR ARGS => .K ... + _ => + #let DATA_OFFSET = #asWord(#range(ARGS, 64, 32)) #in + #let DATA_SIZE = #range(ARGS, DATA_OFFSET, 32) #in + #let DATA = #range(ARGS, DATA_OFFSET +Int 32, #asWord(DATA_SIZE) *Int 32) #in + #let HEAD = Int2Bytes(32, 32, BE) #in + #let BODY = DATA_SIZE +Bytes DATA #in + HEAD +Bytes BODY + + requires SELECTOR in ( + SetItem( selector ( "envOr(string,string,bool[])" ) ) + SetItem( selector ( "envOr(string,string,uint256[])" ) ) + SetItem( selector ( "envOr(string,string,int256[])" ) ) + SetItem( selector ( "envOr(string,string,address[])" ) ) + SetItem( selector ( "envOr(string,string,bytes32[])" ) ) + ) + [preserves-definedness] + + rule [envOr-dynamic-array]: + #cheatcode_call SELECTOR ARGS => .K ... + _ => + #let DATA_OFFSET = #asWord(#range(ARGS, 64, 32)) #in + #let DATA_SIZE = #range(ARGS, DATA_OFFSET, 32) #in + #let DATA = #range(ARGS, DATA_OFFSET +Int 32, #asWord(DATA_SIZE) *Int 32) #in + #let HEAD = Int2Bytes(32, 32, BE) #in + #let BODY = DATA_SIZE +Bytes DATA #in + HEAD +Bytes BODY + + requires SELECTOR in ( + SetItem( selector ( "envOr(string,string,string[])" ) ) + SetItem( selector ( "envOr(string,string,bytes[])" ) ) + ) + [preserves-definedness] +``` + Expecting the next call to revert --------------------------------- @@ -1848,6 +1926,60 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa _ : WS => 1 : WS ``` +- `#getEnvOrValue` will get the return the environment variable from the `` mapping iif it's there, or will return the default value for the variable + +```k + syntax KItem ::= "#getEnvOrValue" Int Bytes Bytes [symbol(foundry_getEnvOrValue)] + // ----------------------------------------------------------------------------- + rule #getEnvOrValue SELECTOR VARNAME VARDEFAULTVALUE => #processOutput SELECTOR VARVALUE VARDEFAULTVALUE ... + ... VARNAME |-> VARVALUE ... + + rule #getEnvOrValue _ _ VARDEFAULTVALUE => .K ... + _ => VARDEFAULTVALUE + [owise] +``` + +```k + syntax KItem ::= "#processOutput" Int String Bytes [symbol(foundry_processOutputAsInt)] + // ----------------------------------------------------------------------------- + rule #processOutput SELECTOR VARVALUE _ => .K ... + _ => Int2Bytes(32, String2Int(VARVALUE), BE) + requires SELECTOR ==Int selector ( "envOr(string,int256)" ) andBool isIntegerString(VARVALUE) + + rule #processOutput SELECTOR VARVALUE _ => .K ... + _ => Int2Bytes(32, String2Int(VARVALUE), BE) + requires SELECTOR ==Int selector ( "envOr(string,uint256)" ) andBool isUnsignedIntegerString(VARVALUE) + + rule #processOutput SELECTOR VARVALUE _ => .K ... + _ => Int2Bytes(32, #parseHexWord(VARVALUE), BE) + requires SELECTOR ==Int selector ( "envOr(string,address)" ) andBool (lengthString(VARVALUE) ==Int 42 orBool lengthString(VARVALUE) ==Int 40) + + rule #processOutput SELECTOR VARVALUE _ => .K ... + _ => Int2Bytes(32, #parseHexWord(VARVALUE), BE) + requires SELECTOR ==Int selector ( "envOr(string,bytes32)" ) andBool (lengthString(VARVALUE) ==Int 66 orBool lengthString(VARVALUE) ==Int 64) + + rule #processOutput SELECTOR VARVALUE _ => .K ... + _ => Int2Bytes(32, bool2Word( String2Bool(VARVALUE) ), BE) + requires SELECTOR ==Int selector ( "envOr(string,bool)" ) andBool (VARVALUE ==K "true" orBool VARVALUE ==K "false") + + rule #processOutput _ _ VARDEFAULTVALUE => .K ... + _ => VARDEFAULTVALUE + [owise] +``` + +```k +syntax Bool ::= isIntegerString(String) [function] + +rule isIntegerString(S) => true requires String2Int(S) ==K 0 orBool String2Int(S) =/=K 0 +rule isIntegerString(_) => false [owise] + +syntax Bool ::= isUnsignedIntegerString(String) [function] + +rule isUnsignedIntegerString(S) => true requires String2Int(S) >=Int 0 +rule isUnsignedIntegerString(_) => false [owise] +``` + + Selectors --------- @@ -1920,6 +2052,20 @@ Selectors for **implemented** cheat code functions. rule ( selector ( "toString(bool)" ) => 1910302682 ) rule ( selector ( "toString(uint256)" ) => 1761649582 ) rule ( selector ( "toString(int256)" ) => 2736964622 ) + rule ( selector ( "envOr(string,address)" ) => 1444930880 ) + rule ( selector ( "envOr(string,bool)" ) => 1199043535 ) + rule ( selector ( "envOr(string,bytes)" ) => 3018094341 ) + rule ( selector ( "envOr(string,bytes32)" ) => 3030931602 ) + rule ( selector ( "envOr(string,int256)" ) => 3150672190 ) + rule ( selector ( "envOr(string,string)" ) => 3510989676 ) + rule ( selector ( "envOr(string,string,address[])" ) => 3343818219 ) + rule ( selector ( "envOr(string,string,bool[])" ) => 3951421499 ) + rule ( selector ( "envOr(string,string,bytes32[])" ) => 578941799 ) + rule ( selector ( "envOr(string,string,bytes[])" ) => 1690058340 ) + rule ( selector ( "envOr(string,string,int256[])" ) => 1191237451 ) + rule ( selector ( "envOr(string,string,string[])" ) => 2240943804 ) + rule ( selector ( "envOr(string,string,uint256[])" ) => 1949402408 ) + rule ( selector ( "envOr(string,uint256)" ) => 1586967695 ) ``` Selectors for **unimplemented** cheat code functions. @@ -1985,4 +2131,4 @@ Selector for Solidity built-in Error ``` ```k endmodule -``` +``` \ No newline at end of file diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 0f7202f1b..df5be8d38 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -39,7 +39,7 @@ from .natspec import apply_natspec_preconditions from .options import ConfigType from .solc_to_k import Contract, decode_kinner_output -from .utils import console, parse_test_version_tuple, replace_k_words +from .utils import console, parse_foundry_env, parse_test_version_tuple, replace_k_words if TYPE_CHECKING: from collections.abc import Iterable @@ -1003,8 +1003,16 @@ def _init_cterm( 'ALLOWEDCALLSLIST_CELL': list_empty(), 'MOCKCALLS_CELL': KApply('.MockCallCellMap'), 'MOCKFUNCTIONS_CELL': KApply('.MockFunctionCellMap'), + 'ENVVARS_CELL': KApply('.Map'), } + # Initialize ENVVARS_CELL with environment variables from .env file + env_vars = parse_foundry_env(foundry._root) + env_map = map_empty() + for key, value in env_vars.items(): + env_map = KApply('_Map_', [map_item(bytesToken(key.encode('utf-8')), token(value)), env_map]) + init_subst['ENVVARS_CELL'] = env_map + storage_constraints: list[KApply] = [] if config_type == ConfigType.TEST_CONFIG or active_simbolik: diff --git a/src/kontrol/utils.py b/src/kontrol/utils.py index 2cdc91f85..d7d278778 100644 --- a/src/kontrol/utils.py +++ b/src/kontrol/utils.py @@ -331,6 +331,42 @@ def decode_log_message(token: str, selector: int) -> str | None: return None +def parse_env_file(file_path: Path) -> dict[str, str]: + """Parse a .env file into a dictionary of key-value pairs. + + :param file_path: Path to the .env file + :return: Dictionary with environment variable names as keys and their values as strings + """ + env_vars = {} + if not file_path.exists(): + return env_vars + with open(file_path, 'r', encoding='utf-8') as f: + for line in f: + line = line.strip() + if not line or line.startswith('#'): + continue + if '=' not in line: + continue + key, value = line.split('=', 1) + key = key.strip() + value = value.strip() + # Remove surrounding quotes if present + if (value.startswith('"') and value.endswith('"')) or (value.startswith("'") and value.endswith("'")): + value = value[1:-1] + env_vars[key] = value + return env_vars + + +def parse_foundry_env(foundry_root: Path) -> dict[str, str]: + """Parse the .env file located in the Foundry root directory. + + :param foundry_root: Path to the Foundry project root directory + :return: Dictionary with environment variable names as keys and their values as strings + """ + env_file = foundry_root / '.env' + return parse_env_file(env_file) + + EMPTY_LOG_SELECTOR = 1368866505 # a mapping from function selectors to the argument types used in the log functions from # https://github.com/foundry-rs/forge-std/blob/ee93fdc45d1e5e4dee883afe0103109881a83549/src/console.sol diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all index c37ddfc25..4060338db 100644 --- a/src/tests/integration/test-data/foundry-prove-all +++ b/src/tests/integration/test-data/foundry-prove-all @@ -100,6 +100,15 @@ EnvTest.testEnvString() EnvTest.testEnvStringArray() EnvTest.testEnvUInt() EnvTest.testEnvUIntArray() +EnvOrTest.testEnvOrUint256() +EnvOrTest.testEnvOrInt256() +EnvOrTest.testEnvOrAddress() +EnvOrTest.testEnvOrBytes32() +EnvOrTest.testEnvOrBool() +EnvOrTest.testEnvOrString() +EnvOrTest.testEnvOrBytes() +EnvOrTest.testEnvOrUint256Array() +EnvOrTest.testEnvOrStringArray() ExpectCallTest.testExpectRegularCall() ExpectCallTest.testExpectStaticCall() ExpectRevertTest.test_expectRevert_bytes4() diff --git a/src/tests/integration/test-data/foundry/test/EnvOrTest.t.sol b/src/tests/integration/test-data/foundry/test/EnvOrTest.t.sol new file mode 100644 index 000000000..f704f3337 --- /dev/null +++ b/src/tests/integration/test-data/foundry/test/EnvOrTest.t.sol @@ -0,0 +1,142 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity =0.8.13; + +import "forge-std/Test.sol"; + +contract EnvOrTest is Test { + + function testEnvOrUint256() public view { + uint256 defaultValue = 42; + uint256 value = vm.envOr("UINT256", defaultValue); + assertEq(100, value); + } + + function testEnvOrUint256Default() public view { + uint256 defaultValue = 42; + uint256 value = vm.envOr("DEFAULT", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrUint256Bad() public view { + uint256 defaultValue = 42; + uint256 value = vm.envOr("BADUINT256", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrInt256() public view { + int256 defaultValue = -42; + int256 value = vm.envOr("INT256", defaultValue); + assertEq(-100, value); + } + + function testEnvOrInt256Default() public view { + int256 defaultValue = -42; + int256 value = vm.envOr("DEFAULT", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrInt256Bad() public view { + int256 defaultValue = -42; + int256 value = vm.envOr("BADINT256", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrAddress() public view { + address defaultValue = address(0x0); + address value = vm.envOr("ADDRESS", defaultValue); + assertEq(address(0x1234567890123456789012345678901234567890), value); + } + + function testEnvOrAddressInt() public view { + address defaultValue = address(0x0); + address value = vm.envOr("ADDRESSINT", defaultValue); + assertEq(address(0x7584896468543216876435687541650546890874), value); + } + + function testEnvOrAddressDefault() public view { + address defaultValue = address(0x123); + address value = vm.envOr("DEFAULT", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrAddressBad() public view { + address defaultValue = address(0x123); + address value = vm.envOr("BADADDRESS", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrBytes32() public view{ + bytes32 defaultValue = bytes32("default"); + bytes32 value = vm.envOr("BYTES32", defaultValue); + bytes32 envVarValue = 0x123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0; + assertEq(envVarValue, value); + } + + function testEnvOrBytes32Default() public view{ + bytes32 defaultValue = bytes32("default"); + bytes32 value = vm.envOr("DEFAULT", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrBytes32Bad() public view{ + bytes32 defaultValue = bytes32("default"); + bytes32 value = vm.envOr("BADBYTES32", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrBool() public view { + bool trueValue = vm.envOr("BOOLTRUE", false); + assertEq(trueValue, true); + bool falseValue = vm.envOr("BOOLFALSE", true); + assertEq(falseValue, false); + } + + function testEnvOrBoolDefault() public view { + bool trueValue = vm.envOr("DEFAULT", true); + assertEq(trueValue, true); + bool falseValue = vm.envOr("DEFAULT", false); + assertEq(falseValue, false); + } + + function testEnvOrBoolBad() public view { + bool trueValue = vm.envOr("BADBOOLTRUE", true); + assertEq(trueValue, true); + bool falseValue = vm.envOr("BADBOOLFALSE", false); + assertEq(falseValue, false); + } + + function testEnvOrBytes() public view { + bytes memory defaultValue = "default"; + bytes memory value = vm.envOr("ANY", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrString() public view { + string memory defaultValue = "default"; + string memory value = vm.envOr("ANY", defaultValue); + assertEq(defaultValue, value); + } + + function testEnvOrUint256Array() public view { + uint256[] memory defaultValue = new uint256[](2); + defaultValue[0] = 1; + defaultValue[1] = 2; + uint256[] memory value = vm.envOr("ANY", ",", defaultValue); + assertEq(defaultValue.length, value.length); + for (uint256 i = 0; i < defaultValue.length; i++) { + assertEq(defaultValue[i], value[i]); + } + } + + function testEnvOrStringArray() public view { + string[] memory defaultValue = new string[](2); + defaultValue[0] = "one"; + defaultValue[1] = "two"; + string[] memory value = vm.envOr("ANY", ",", defaultValue); + assertEq(defaultValue.length, value.length); + for (uint256 i = 0; i < defaultValue.length; i++) { + assertEq(defaultValue[i], value[i]); + } + } + +} \ No newline at end of file