Skip to content

Commit

Permalink
Merge branch 'master' into chore/expand-cancellation-ability
Browse files Browse the repository at this point in the history
  • Loading branch information
arr00 authored Nov 18, 2024
2 parents 0afbab5 + 448efee commit c8412b7
Show file tree
Hide file tree
Showing 20 changed files with 238 additions and 133 deletions.
44 changes: 26 additions & 18 deletions certora/run.js
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,16 @@
// node certora/run.js AccessControl
// node certora/run.js AccessControlHarness:AccessControl

const proc = require('child_process');
const { PassThrough } = require('stream');
const events = require('events');

const argv = require('yargs')
import { spawn } from 'child_process';
import { PassThrough } from 'stream';
import { once } from 'events';
import path from 'path';
import yargs from 'yargs';
import { hideBin } from 'yargs/helpers';
import pLimit from 'p-limit';
import fs from 'fs/promises';

const argv = yargs(hideBin(process.argv))
.env('')
.options({
all: {
Expand All @@ -21,7 +26,7 @@ const argv = require('yargs')
spec: {
alias: 's',
type: 'string',
default: __dirname + '/specs.json',
default: path.resolve(import.meta.dirname, 'specs.json'),
},
parallel: {
alias: 'p',
Expand All @@ -38,18 +43,20 @@ const argv = require('yargs')
type: 'array',
default: [],
},
}).argv;
})
.parse();

function match(entry, request) {
const [reqSpec, reqContract] = request.split(':').reverse();
return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract);
}

const specs = require(argv.spec).filter(s => argv.all || argv._.some(r => match(s, r)));
const limit = require('p-limit')(argv.parallel);
const specs = JSON.parse(fs.readFileSync(argv.spec, 'utf8')).filter(s => argv.all || argv._.some(r => match(s, r)));

const limit = pLimit(argv.parallel);

if (argv._.length == 0 && !argv.all) {
console.error(`Warning: No specs requested. Did you forgot to toggle '--all'?`);
console.error(`Warning: No specs requested. Did you forget to toggle '--all'?`);
}

for (const r of argv._) {
Expand All @@ -64,12 +71,13 @@ if (process.exitCode) {
}

for (const { spec, contract, files, options = [] } of specs) {
limit(
runCertora,
spec,
contract,
files,
[...options, ...argv.options].flatMap(opt => opt.split(' ')),
limit(() =>
runCertora(
spec,
contract,
files,
[...options, ...argv.options].flatMap(opt => opt.split(' ')),
),
);
}

Expand All @@ -79,7 +87,7 @@ async function runCertora(spec, contract, files, options = []) {
if (argv.verbose) {
console.log('Running:', args.join(' '));
}
const child = proc.spawn('certoraRun', args);
const child = spawn('certoraRun', args);

const stream = new PassThrough();
const output = collect(stream);
Expand All @@ -103,7 +111,7 @@ async function runCertora(spec, contract, files, options = []) {
});

// wait for process end
const [code, signal] = await events.once(child, 'exit');
const [code, signal] = await once(child, 'exit');

// error
if (code || signal) {
Expand Down
72 changes: 38 additions & 34 deletions contracts/utils/math/Math.sol
Original file line number Diff line number Diff line change
Expand Up @@ -537,41 +537,45 @@ library Math {
* @dev Return the log in base 2 of a positive value rounded towards zero.
* Returns 0 if given 0.
*/
function log2(uint256 value) internal pure returns (uint256) {
uint256 result = 0;
uint256 exp;
unchecked {
exp = 128 * SafeCast.toUint(value > (1 << 128) - 1);
value >>= exp;
result += exp;

exp = 64 * SafeCast.toUint(value > (1 << 64) - 1);
value >>= exp;
result += exp;

exp = 32 * SafeCast.toUint(value > (1 << 32) - 1);
value >>= exp;
result += exp;

exp = 16 * SafeCast.toUint(value > (1 << 16) - 1);
value >>= exp;
result += exp;

exp = 8 * SafeCast.toUint(value > (1 << 8) - 1);
value >>= exp;
result += exp;

exp = 4 * SafeCast.toUint(value > (1 << 4) - 1);
value >>= exp;
result += exp;

exp = 2 * SafeCast.toUint(value > (1 << 2) - 1);
value >>= exp;
result += exp;

result += SafeCast.toUint(value > 1);
function log2(uint256 x) internal pure returns (uint256 r) {
// If value has upper 128 bits set, log2 result is at least 128
r = SafeCast.toUint(x > 0xffffffffffffffffffffffffffffffff) << 7;
// If upper 64 bits of 128-bit half set, add 64 to result
r |= SafeCast.toUint((x >> r) > 0xffffffffffffffff) << 6;
// If upper 32 bits of 64-bit half set, add 32 to result
r |= SafeCast.toUint((x >> r) > 0xffffffff) << 5;
// If upper 16 bits of 32-bit half set, add 16 to result
r |= SafeCast.toUint((x >> r) > 0xffff) << 4;
// If upper 8 bits of 16-bit half set, add 8 to result
r |= SafeCast.toUint((x >> r) > 0xff) << 3;
// If upper 4 bits of 8-bit half set, add 4 to result
r |= SafeCast.toUint((x >> r) > 0xf) << 2;

// Shifts value right by the current result and use it as an index into this lookup table:
//
// | x (4 bits) | index | table[index] = MSB position |
// |------------|---------|-----------------------------|
// | 0000 | 0 | table[0] = 0 |
// | 0001 | 1 | table[1] = 0 |
// | 0010 | 2 | table[2] = 1 |
// | 0011 | 3 | table[3] = 1 |
// | 0100 | 4 | table[4] = 2 |
// | 0101 | 5 | table[5] = 2 |
// | 0110 | 6 | table[6] = 2 |
// | 0111 | 7 | table[7] = 2 |
// | 1000 | 8 | table[8] = 3 |
// | 1001 | 9 | table[9] = 3 |
// | 1010 | 10 | table[10] = 3 |
// | 1011 | 11 | table[11] = 3 |
// | 1100 | 12 | table[12] = 3 |
// | 1101 | 13 | table[13] = 3 |
// | 1110 | 14 | table[14] = 3 |
// | 1111 | 15 | table[15] = 3 |
//
// The lookup table is represented as a 32-byte value with the MSB positions for 0-15 in the last 16 bytes.
assembly ("memory-safe") {
r := or(r, byte(shr(r, x), 0x0000010102020202030303030303030300000000000000000000000000000000))
}
return result;
}

/**
Expand Down
2 changes: 1 addition & 1 deletion lib/forge-std
Submodule forge-std updated 6 files
+193 −0 CONTRIBUTING.md
+16 −0 README.md
+1 −1 package.json
+12 −1 scripts/vm.py
+126 −16 src/Vm.sol
+2 −2 test/Vm.t.sol
109 changes: 99 additions & 10 deletions package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion package.json
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@
"hardhat-ignore-warnings": "^0.2.11",
"lodash.startcase": "^4.4.0",
"micromatch": "^4.0.2",
"p-limit": "^3.1.0",
"p-limit": "^6.0.0",
"prettier": "^3.0.0",
"prettier-plugin-solidity": "^1.1.0",
"rimraf": "^6.0.0",
Expand Down
2 changes: 1 addition & 1 deletion scripts/generate/templates/Checkpoints.t.js
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ function _prepareKeys(${opts.keyTypeName}[] memory keys, ${opts.keyTypeName} max
}
}
function _assertLatestCheckpoint(bool exist, ${opts.keyTypeName} key, ${opts.valueTypeName} value) internal {
function _assertLatestCheckpoint(bool exist, ${opts.keyTypeName} key, ${opts.valueTypeName} value) internal view {
(bool _exist, ${opts.keyTypeName} _key, ${opts.valueTypeName} _value) = _ckpts.latestCheckpoint();
assertEq(_exist, exist);
assertEq(_key, key);
Expand Down
Loading

0 comments on commit c8412b7

Please sign in to comment.