1use super::{INLINE_CONFIG_PREFIX, InlineConfigError, InlineConfigErrorKind};
2use crate::split_quoted_args;
3use figment::Profile;
4use foundry_compilers::{
5 ProjectCompileOutput,
6 artifacts::{Node, ast::NodeType},
7};
8use itertools::Itertools;
9use serde_json::Value;
10use solar::{
11 ast::{self, Span},
12 interface::Session,
13};
14use std::{collections::BTreeMap, path::Path};
15
16const HALMOS_CONFIG_PREFIX: &str = "@custom:halmos";
17
18#[derive(Clone, Debug, PartialEq, Eq)]
20pub struct NatSpec {
21 pub contract: String,
23 pub function: Option<String>,
25 pub line: String,
27 pub docs: String,
29}
30
31impl NatSpec {
32 #[instrument(name = "NatSpec::parse", skip_all)]
36 pub fn parse(output: &ProjectCompileOutput, root: &Path) -> Vec<Self> {
37 let mut natspecs: Vec<Self> = vec![];
38
39 let compiler = output.parser().solc().compiler();
40 let solar = SolarParser::new(compiler.sess());
41 let solc = SolcParser::new();
42 for (id, artifact) in output.artifact_ids() {
43 let path = id.source.as_path();
44 let path = path.strip_prefix(root).unwrap_or(path);
45 let abs_path = &*root.join(path);
46 let contract_name = id.name.split('.').next().unwrap();
47 let contract = format!("{}:{}", path.display(), id.name);
49
50 let mut used_solar = false;
51 compiler.enter_sequential(|compiler| {
52 if let Some((_, source)) = compiler.gcx().get_ast_source(abs_path)
53 && let Some(ast) = &source.ast
54 {
55 solar.parse_ast(&mut natspecs, ast, &contract, contract_name);
56 used_solar = true;
57 }
58 });
59
60 if !used_solar {
61 warn!(?abs_path, %contract, "could not parse natspec with solar");
62 }
63
64 let used_solc = if !used_solar
65 && let Some(ast) = &artifact.ast
66 && let Some(node) = solc.contract_root_node(&ast.nodes, &contract)
67 {
68 solc.parse(&mut natspecs, &contract, node, true);
69 true
70 } else {
71 false
72 };
73
74 if !used_solar && !used_solc {
75 warn!(?abs_path, %contract, "could not parse natspec");
76 }
77 }
78
79 natspecs
80 }
81
82 pub fn validate_profiles(&self, profiles: &[Profile]) -> eyre::Result<()> {
91 for config in self.config_values() {
92 if !profiles.iter().any(|p| {
93 config
94 .strip_prefix(p.as_str().as_str())
95 .is_some_and(|rest| rest.trim_start().starts_with('.'))
96 }) {
97 Err(InlineConfigError {
98 location: self.location_string(),
99 kind: InlineConfigErrorKind::InvalidProfile(
100 config.to_string(),
101 profiles.iter().format(", ").to_string(),
102 ),
103 })?
104 }
105 }
106 Ok(())
107 }
108
109 pub fn path(&self) -> &str {
111 match self.contract.split_once(':') {
112 Some((path, _)) => path,
113 None => self.contract.as_str(),
114 }
115 }
116
117 pub fn location_string(&self) -> String {
119 format!("{}:{}", self.path(), self.line)
120 }
121
122 pub fn config_values(&self) -> impl Iterator<Item = &str> {
124 self.docs.lines().filter_map(|line| {
125 line.find(INLINE_CONFIG_PREFIX)
126 .map(|idx| line[idx + INLINE_CONFIG_PREFIX.len()..].trim())
127 })
128 }
129
130 pub fn halmos_config_values(&self) -> Result<Vec<String>, InlineConfigError> {
135 let mut values = Vec::new();
136 for line in self.docs.lines() {
137 let Some(idx) = line.find(HALMOS_CONFIG_PREFIX) else { continue };
138 let args = line[idx + HALMOS_CONFIG_PREFIX.len()..].trim();
139 translate_halmos_config(args, &mut values).map_err(|message| InlineConfigError {
140 location: self.location_string(),
141 kind: InlineConfigErrorKind::InvalidHalmosConfig(message),
142 })?;
143 }
144 Ok(values)
145 }
146}
147
148fn translate_halmos_config(args: &str, values: &mut Vec<String>) -> Result<(), String> {
149 let tokens = split_halmos_args(args)?;
150 let mut idx = 0;
151 while idx < tokens.len() {
152 let token = tokens[idx].as_str();
153 if token == "--array-lengths" {
154 idx += 1;
155 let Some(value) = tokens.get(idx) else {
156 return Err("missing value for --array-lengths".to_string());
157 };
158 push_halmos_array_lengths(values, value)?;
159 } else if let Some(value) = token.strip_prefix("--array-lengths=") {
160 push_halmos_array_lengths(values, value)?;
161 } else if token == "--default-array-lengths" {
162 idx += 1;
163 let Some(value) = tokens.get(idx) else {
164 return Err("missing value for --default-array-lengths".to_string());
165 };
166 push_halmos_lengths(values, "default_array_lengths", value, "--default-array-lengths")?;
167 } else if let Some(value) = token.strip_prefix("--default-array-lengths=") {
168 push_halmos_lengths(values, "default_array_lengths", value, "--default-array-lengths")?;
169 } else if token == "--default-bytes-lengths" {
170 idx += 1;
171 let Some(value) = tokens.get(idx) else {
172 return Err("missing value for --default-bytes-lengths".to_string());
173 };
174 push_halmos_lengths(values, "default_bytes_lengths", value, "--default-bytes-lengths")?;
175 } else if let Some(value) = token.strip_prefix("--default-bytes-lengths=") {
176 push_halmos_lengths(values, "default_bytes_lengths", value, "--default-bytes-lengths")?;
177 } else if let Some(field) = halmos_numeric_symbolic_field(token) {
178 idx += 1;
179 let Some(value) = tokens.get(idx) else {
180 return Err(format!("missing value for {token}"));
181 };
182 push_halmos_u32(values, field, value, token)?;
183 } else if let Some(value) = token.strip_prefix("--invariant-depth=") {
184 push_halmos_u32(values, "invariant_depth", value, "--invariant-depth")?;
185 } else if let Some(value) = token.strip_prefix("--loop=") {
186 push_halmos_u32(values, "loop", value, "--loop")?;
187 } else if let Some(value) = token.strip_prefix("--width=") {
188 push_halmos_u32(values, "width", value, "--width")?;
189 } else if let Some(value) = token.strip_prefix("--depth=") {
190 push_halmos_u32(values, "depth", value, "--depth")?;
191 } else if let Some(value) = token.strip_prefix("--solver-timeout=") {
192 push_halmos_u32(values, "timeout", value, "--solver-timeout")?;
193 } else if let Some(value) = token.strip_prefix("--solver-timeout-branching=") {
194 push_halmos_u32(values, "timeout", value, "--solver-timeout-branching")?;
195 } else if let Some(value) = token.strip_prefix("--solver-timeout-assertion=") {
196 push_halmos_u32(values, "timeout", value, "--solver-timeout-assertion")?;
197 } else if token == "--solver" {
198 idx += 1;
199 let Some(value) = tokens.get(idx) else {
200 return Err("missing value for --solver".to_string());
201 };
202 push_halmos_string(values, "solver", value);
203 } else if let Some(value) = token.strip_prefix("--solver=") {
204 push_halmos_string(values, "solver", value);
205 } else if token == "--solver-command" {
206 idx += 1;
207 let Some(value) = tokens.get(idx) else {
208 return Err("missing value for --solver-command".to_string());
209 };
210 push_halmos_string(values, "solver_command", value);
211 } else if let Some(value) = token.strip_prefix("--solver-command=") {
212 push_halmos_string(values, "solver_command", value);
213 } else if token.starts_with("--")
214 && tokens.get(idx + 1).is_some_and(|next| !next.starts_with("--"))
215 {
216 idx += 1;
217 }
218 idx += 1;
219 }
220 Ok(())
221}
222
223fn split_halmos_args(args: &str) -> Result<Vec<String>, String> {
224 split_quoted_args(args)
225 .map_err(|quote_ch| format!("unterminated {quote_ch} quote in @custom:halmos config"))
226}
227
228fn halmos_numeric_symbolic_field(flag: &str) -> Option<&'static str> {
229 match flag {
230 "--loop" => Some("loop"),
231 "--width" => Some("width"),
232 "--depth" => Some("depth"),
233 "--invariant-depth" => Some("invariant_depth"),
234 "--solver-timeout" | "--solver-timeout-branching" | "--solver-timeout-assertion" => {
235 Some("timeout")
236 }
237 _ => None,
238 }
239}
240
241fn push_halmos_array_lengths(values: &mut Vec<String>, value: &str) -> Result<(), String> {
242 match parse_halmos_array_lengths(value)? {
243 HalmosArrayLengths::Positional(lengths) => {
244 values.push(format!(
245 "default.symbolic.array_lengths = [{}]",
246 lengths.iter().format(", ")
247 ));
248 }
249 HalmosArrayLengths::Named(lengths) => {
250 values.push(format!(
251 "default.symbolic.dynamic_lengths = {{ {} }}",
252 lengths
253 .iter()
254 .map(|(name, lengths)| format!("{name} = [{}]", lengths.iter().format(", ")))
255 .format(", ")
256 ));
257 }
258 }
259 Ok(())
260}
261
262fn push_halmos_lengths(
263 values: &mut Vec<String>,
264 field: &str,
265 value: &str,
266 flag: &str,
267) -> Result<(), String> {
268 values.push(format!(
269 "default.symbolic.{field} = [{}]",
270 parse_halmos_lengths(value, flag)?.iter().format(", ")
271 ));
272 Ok(())
273}
274
275fn push_halmos_u32(
276 values: &mut Vec<String>,
277 field: &str,
278 value: &str,
279 flag: &str,
280) -> Result<(), String> {
281 values.push(format!("default.symbolic.{field} = {}", parse_halmos_u32(value, flag)?));
282 Ok(())
283}
284
285fn push_halmos_string(values: &mut Vec<String>, field: &str, value: &str) {
286 values.push(format!("default.symbolic.{field} = {}", toml_string(value)));
287}
288
289fn toml_string(value: &str) -> String {
290 format!("\"{}\"", value.replace('\\', "\\\\").replace('"', "\\\""))
291}
292
293fn parse_halmos_u32(value: &str, flag: &str) -> Result<u32, String> {
294 value.parse::<u32>().map_err(|_| format!("invalid value `{value}` for {flag}"))
295}
296
297enum HalmosArrayLengths {
298 Positional(Vec<u32>),
299 Named(BTreeMap<String, Vec<u32>>),
300}
301
302fn parse_halmos_array_lengths(value: &str) -> Result<HalmosArrayLengths, String> {
303 if value.contains('=') {
304 let mut named = BTreeMap::new();
305 for entry in split_halmos_lengths_entries(value)? {
306 let Some((name, lengths)) = entry.split_once('=') else {
307 return Err(format!(
308 "mixed named and positional lengths in --array-lengths `{value}`"
309 ));
310 };
311 let name = name.trim();
312 if name.is_empty() {
313 return Err(format!("missing name in --array-lengths `{value}`"));
314 }
315 named.insert(
316 name.to_string(),
317 parse_halmos_length_set(lengths.trim(), "--array-lengths")?,
318 );
319 }
320 if named.is_empty() {
321 return Err("missing value for --array-lengths".to_string());
322 }
323 Ok(HalmosArrayLengths::Named(named))
324 } else {
325 Ok(HalmosArrayLengths::Positional(parse_halmos_lengths(value, "--array-lengths")?))
326 }
327}
328
329fn parse_halmos_lengths(value: &str, flag: &str) -> Result<Vec<u32>, String> {
330 parse_halmos_length_set(value, flag)
331}
332
333fn parse_halmos_length_set(value: &str, flag: &str) -> Result<Vec<u32>, String> {
334 let value = value.trim();
335 let value = value.strip_prefix('{').and_then(|value| value.strip_suffix('}')).unwrap_or(value);
336 let mut lengths = Vec::new();
337 for length in value.split(',') {
338 let length = length.trim();
339 if length.is_empty() {
340 return Err(format!("invalid empty length in {flag} `{value}`"));
341 }
342 let length = length
343 .parse::<u32>()
344 .map_err(|_| format!("invalid length `{length}` in {flag} `{value}`"))?;
345 lengths.push(length);
346 }
347 if lengths.is_empty() {
348 return Err(format!("missing value for {flag}"));
349 }
350 Ok(lengths)
351}
352
353fn split_halmos_lengths_entries(value: &str) -> Result<Vec<&str>, String> {
354 let mut entries = Vec::new();
355 let mut start = 0usize;
356 let mut brace_depth = 0u8;
357 for (idx, ch) in value.char_indices() {
358 match ch {
359 '{' => brace_depth = brace_depth.saturating_add(1),
360 '}' => {
361 brace_depth = brace_depth
362 .checked_sub(1)
363 .ok_or_else(|| format!("unmatched `}}` in --array-lengths `{value}`"))?;
364 }
365 ',' if brace_depth == 0 => {
366 entries.push(value[start..idx].trim());
367 start = idx + 1;
368 }
369 _ => {}
370 }
371 }
372 if brace_depth != 0 {
373 return Err(format!("unmatched `{{` in --array-lengths `{value}`"));
374 }
375 entries.push(value[start..].trim());
376 Ok(entries)
377}
378
379struct SolcParser {
380 _private: (),
381}
382
383impl SolcParser {
384 const fn new() -> Self {
385 Self { _private: () }
386 }
387
388 fn contract_root_node<'a>(&self, nodes: &'a [Node], contract_id: &str) -> Option<&'a Node> {
391 for n in nodes {
392 if n.node_type == NodeType::ContractDefinition {
393 let contract_data = &n.other;
394 if let Value::String(contract_name) = contract_data.get("name")?
395 && contract_id.ends_with(contract_name)
396 {
397 return Some(n);
398 }
399 }
400 }
401 None
402 }
403
404 fn parse(&self, natspecs: &mut Vec<NatSpec>, contract: &str, node: &Node, root: bool) {
407 if root && let Some((docs, line)) = self.get_node_docs(&node.other) {
409 natspecs.push(NatSpec { contract: contract.into(), function: None, docs, line })
410 }
411 for n in &node.nodes {
412 if let Some((function, docs, line)) = self.get_fn_data(n) {
413 natspecs.push(NatSpec {
414 contract: contract.into(),
415 function: Some(function),
416 line,
417 docs,
418 })
419 }
420 self.parse(natspecs, contract, n, false);
421 }
422 }
423
424 fn get_fn_data(&self, node: &Node) -> Option<(String, String, String)> {
432 if node.node_type == NodeType::FunctionDefinition {
433 let fn_data = &node.other;
434 let fn_name: String = self.get_fn_name(fn_data)?;
435 let (fn_docs, docs_src_line) = self.get_node_docs(fn_data)?;
436 return Some((fn_name, fn_docs, docs_src_line));
437 }
438
439 None
440 }
441
442 fn get_fn_name(&self, fn_data: &BTreeMap<String, Value>) -> Option<String> {
444 match fn_data.get("name")? {
445 Value::String(fn_name) => Some(fn_name.into()),
446 _ => None,
447 }
448 }
449
450 fn get_node_docs(&self, data: &BTreeMap<String, Value>) -> Option<(String, String)> {
456 if let Value::Object(fn_docs) = data.get("documentation")?
457 && let Value::String(comment) = fn_docs.get("text")?
458 && contains_inline_config(comment)
459 {
460 let mut src_line = fn_docs
461 .get("src")
462 .map(|src| src.to_string())
463 .unwrap_or_else(|| String::from("<no-src-line-available>"));
464
465 src_line.retain(|c| c != '"');
466 return Some((comment.into(), src_line));
467 }
468 None
469 }
470}
471
472struct SolarParser<'a> {
473 sess: &'a Session,
474}
475
476impl<'a> SolarParser<'a> {
477 const fn new(sess: &'a Session) -> Self {
478 Self { sess }
479 }
480
481 fn parse_ast(
482 &self,
483 natspecs: &mut Vec<NatSpec>,
484 source_unit: &ast::SourceUnit<'_>,
485 contract_id: &str,
486 contract_name: &str,
487 ) {
488 let mut handle_docs = |item: &ast::Item<'_>| {
489 if item.docs.is_empty() {
490 return;
491 }
492 let mut span = Span::DUMMY;
493 let lines = item
494 .docs
495 .iter()
496 .filter_map(|d| {
497 let s = d.symbol.as_str();
498 if !contains_inline_config(s) {
499 return None;
500 }
501 span = if span.is_dummy() { d.span } else { span.to(d.span) };
502 match d.kind {
503 ast::CommentKind::Line => Some(s.trim().to_string()),
504 ast::CommentKind::Block => Some(
505 s.lines()
506 .filter(|line| contains_inline_config(line))
507 .map(|line| line.trim_start().trim_start_matches('*').trim())
508 .collect::<Vec<_>>()
509 .join("\n"),
510 ),
511 }
512 })
513 .join("\n");
514 if lines.is_empty() {
515 return;
516 }
517 natspecs.push(NatSpec {
518 contract: contract_id.to_string(),
519 function: if let ast::ItemKind::Function(f) = &item.kind {
520 Some(
521 f.header
522 .name
523 .map(|sym| sym.to_string())
524 .unwrap_or_else(|| f.kind.to_string()),
525 )
526 } else {
527 None
528 },
529 line: {
530 let (_, loc) = self.sess.source_map().span_to_location_info(span);
531 format!("{}:{}", loc.lo.line, loc.lo.col.0 + 1)
532 },
533 docs: lines,
534 });
535 };
536
537 for item in source_unit.items.iter() {
538 let ast::ItemKind::Contract(c) = &item.kind else { continue };
539 if c.name.as_str() != contract_name {
540 continue;
541 }
542
543 handle_docs(item);
545
546 for item in c.body.iter() {
548 let ast::ItemKind::Function(_) = &item.kind else { continue };
549 handle_docs(item);
550 }
551 }
552 }
553}
554
555fn contains_inline_config(s: &str) -> bool {
556 s.contains(INLINE_CONFIG_PREFIX) || s.contains(HALMOS_CONFIG_PREFIX)
557}
558
559#[cfg(test)]
560mod tests {
561 use super::*;
562 use serde_json::json;
563 use snapbox::{assert_data_eq, str};
564 use solar::parse::{
565 Parser,
566 ast::{Arena, interface},
567 };
568
569 fn parse(natspecs: &mut Vec<NatSpec>, src: &str, contract_id: &str, contract_name: &str) {
570 if !contains_inline_config(src) {
572 return;
573 }
574
575 let sess = Session::builder()
576 .with_silent_emitter(Some("Inline config parsing failed".to_string()))
577 .build();
578 let solar = SolarParser::new(&sess);
579 let _ = sess.enter(|| -> interface::Result<()> {
580 let arena = Arena::new();
581
582 let mut parser = Parser::from_source_code(
583 &sess,
584 &arena,
585 interface::source_map::FileName::Custom(contract_id.to_string()),
586 src.to_string(),
587 )?;
588
589 let source_unit = parser.parse_file().map_err(|e| e.emit())?;
590
591 solar.parse_ast(natspecs, &source_unit, contract_id, contract_name);
592
593 Ok(())
594 });
595 }
596
597 #[test]
598 fn can_reject_invalid_profiles() {
599 let profiles = ["ci".into(), "default".into()];
600 let natspec = NatSpec {
601 contract: Default::default(),
602 function: Default::default(),
603 line: Default::default(),
604 docs: r"
605 forge-config: ciii.invariant.depth = 1
606 forge-config: default.invariant.depth = 1
607 "
608 .into(),
609 };
610
611 let result = natspec.validate_profiles(&profiles);
612 assert!(result.is_err());
613 }
614
615 #[test]
616 fn can_accept_valid_profiles() {
617 let profiles = ["ci".into(), "default".into()];
618 let natspec = NatSpec {
619 contract: Default::default(),
620 function: Default::default(),
621 line: Default::default(),
622 docs: r"
623 forge-config: ci.invariant.depth = 1
624 forge-config: default.invariant.depth = 1
625 "
626 .into(),
627 };
628
629 let result = natspec.validate_profiles(&profiles);
630 assert!(result.is_ok());
631 }
632
633 #[test]
634 fn parse_solar() {
635 let src = "
636contract C { /// forge-config: default.fuzz.runs = 600
637
638\t\t\t\t /// forge-config: default.fuzz.runs = 601
639
640 function f1() {}
641 /** forge-config: default.fuzz.runs = 700 */
642function f2() {} /** forge-config: default.fuzz.runs = 800 */ function f3() {}
643
644/**
645 * forge-config: default.fuzz.runs = 1024
646 * forge-config: default.fuzz.max-test-rejects = 500
647 */
648 function f4() {}
649}
650";
651 let mut natspecs = vec![];
652 parse(&mut natspecs, src, "path.sol:C", "C");
653 assert_data_eq!(
654 format!("{natspecs:#?}"),
655 str![[r#"
656[
657 NatSpec {
658 contract: "path.sol:C",
659 function: Some(
660 "f1",
661 ),
662 line: "2:14",
663 docs: "forge-config: default.fuzz.runs = 600/nforge-config: default.fuzz.runs = 601",
664 },
665 NatSpec {
666 contract: "path.sol:C",
667 function: Some(
668 "f2",
669 ),
670 line: "7:8",
671 docs: "forge-config: default.fuzz.runs = 700",
672 },
673 NatSpec {
674 contract: "path.sol:C",
675 function: Some(
676 "f3",
677 ),
678 line: "8:18",
679 docs: "forge-config: default.fuzz.runs = 800",
680 },
681 NatSpec {
682 contract: "path.sol:C",
683 function: Some(
684 "f4",
685 ),
686 line: "10:1",
687 docs: "forge-config: default.fuzz.runs = 1024/nforge-config: default.fuzz.max-test-rejects = 500",
688 },
689]
690"#]]
691 );
692 }
693
694 #[test]
695 fn parse_solar_2() {
696 let src = r#"
697// SPDX-License-Identifier: MIT OR Apache-2.0
698pragma solidity >=0.8.0;
699
700import "ds-test/test.sol";
701
702contract FuzzInlineConf is DSTest {
703 /**
704 * forge-config: default.fuzz.runs = 1024
705 * forge-config: default.fuzz.max-test-rejects = 500
706 */
707 function testInlineConfFuzz(uint8 x) public {
708 require(true, "this is not going to revert");
709 }
710}
711 "#;
712 let mut natspecs = vec![];
713 parse(&mut natspecs, src, "inline/FuzzInlineConf.t.sol:FuzzInlineConf", "FuzzInlineConf");
714 assert_data_eq!(
715 format!("{natspecs:#?}"),
716 str![[r#"
717[
718 NatSpec {
719 contract: "inline/FuzzInlineConf.t.sol:FuzzInlineConf",
720 function: Some(
721 "testInlineConfFuzz",
722 ),
723 line: "8:5",
724 docs: "forge-config: default.fuzz.runs = 1024/nforge-config: default.fuzz.max-test-rejects = 500",
725 },
726]
727"#]]
728 );
729 }
730
731 #[test]
732 fn config_lines() {
733 let natspec = natspec();
734 let config_lines = natspec.config_values();
735 assert_eq!(
736 config_lines.collect::<Vec<_>>(),
737 [
738 "default.fuzz.runs = 600".to_string(),
739 "ci.fuzz.runs = 500".to_string(),
740 "default.invariant.runs = 1".to_string()
741 ]
742 )
743 }
744
745 #[test]
746 fn can_handle_unavailable_src_line_with_fallback() {
747 let mut fn_data: BTreeMap<String, Value> = BTreeMap::new();
748 let doc_without_src_field = json!({ "text": "forge-config:default.fuzz.runs=600" });
749 fn_data.insert("documentation".into(), doc_without_src_field);
750 let (_, src_line) = SolcParser::new().get_node_docs(&fn_data).expect("Some docs");
751 assert_eq!(src_line, "<no-src-line-available>".to_string());
752 }
753
754 #[test]
755 fn can_handle_available_src_line() {
756 let mut fn_data: BTreeMap<String, Value> = BTreeMap::new();
757 let doc_without_src_field =
758 json!({ "text": "forge-config:default.fuzz.runs=600", "src": "73:21:12" });
759 fn_data.insert("documentation".into(), doc_without_src_field);
760 let (_, src_line) = SolcParser::new().get_node_docs(&fn_data).expect("Some docs");
761 assert_eq!(src_line, "73:21:12".to_string());
762 }
763
764 fn natspec() -> NatSpec {
765 let conf = r"
766 forge-config: default.fuzz.runs = 600
767 forge-config: ci.fuzz.runs = 500
768 ========= SOME NOISY TEXT =============
769 䩹𧀫Jx닧Ʀ̳盅K擷Ɂw첊}ꏻk86ᖪk-檻ܴ렝[Dz𐤬oᘓƤ
770 ꣖ۻ%Ƅ㪕ς:(饁av/烲ڻ̛߉橞㗡𥺃̹M봓䀖ؿ̄)d
771 ϊ&»ϿЏ2鞷砕eߥHJ粊머?槿ᴴጅϖ뀓Ӽ츙4
772 醤㭊r ܖ̹灱녗V*竅⒪苏贗=숽ؓбݧʹ園Ьi
773 =======================================
774 forge-config: default.invariant.runs = 1
775 ";
776
777 NatSpec {
778 contract: "dir/TestContract.t.sol:FuzzContract".to_string(),
779 function: Some("test_myFunction".to_string()),
780 line: "10:12:111".to_string(),
781 docs: conf.to_string(),
782 }
783 }
784
785 #[test]
786 fn parse_solar_multiple_contracts_from_same_file() {
787 let src = r#"
788// SPDX-License-Identifier: MIT OR Apache-2.0
789pragma solidity >=0.8.0;
790
791import "ds-test/test.sol";
792
793contract FuzzInlineConf is DSTest {
794 /// forge-config: default.fuzz.runs = 1
795 function testInlineConfFuzz1() {}
796}
797
798contract FuzzInlineConf2 is DSTest {
799 /// forge-config: default.fuzz.runs = 2
800 function testInlineConfFuzz2() {}
801}
802 "#;
803 let mut natspecs = vec![];
804 parse(&mut natspecs, src, "inline/FuzzInlineConf.t.sol:FuzzInlineConf", "FuzzInlineConf");
805 assert_data_eq!(
806 format!("{natspecs:#?}"),
807 str![[r#"
808[
809 NatSpec {
810 contract: "inline/FuzzInlineConf.t.sol:FuzzInlineConf",
811 function: Some(
812 "testInlineConfFuzz1",
813 ),
814 line: "8:6",
815 docs: "forge-config: default.fuzz.runs = 1",
816 },
817]
818"#]]
819 );
820
821 let mut natspecs = vec![];
822 parse(
823 &mut natspecs,
824 src,
825 "inline/FuzzInlineConf2.t.sol:FuzzInlineConf2",
826 "FuzzInlineConf2",
827 );
828 assert_data_eq!(
829 format!("{natspecs:#?}"),
830 str![[r#"
831[
832 NatSpec {
833 contract: "inline/FuzzInlineConf2.t.sol:FuzzInlineConf2",
834 function: Some(
835 "testInlineConfFuzz2",
836 ),
837 line: "13:5",
838 docs: "forge-config: default.fuzz.runs = 2",
839 },
840]
841"#]]
842 );
843 }
844
845 #[test]
846 fn parse_contract_level_config() {
847 let src = r#"
848// SPDX-License-Identifier: MIT OR Apache-2.0
849pragma solidity >=0.8.0;
850
851import "ds-test/test.sol";
852
853/// forge-config: default.fuzz.runs = 1
854contract FuzzInlineConf is DSTest {
855 /// forge-config: default.fuzz.runs = 3
856 function testInlineConfFuzz1() {}
857
858 function testInlineConfFuzz2() {}
859}"#;
860 let mut natspecs = vec![];
861 parse(&mut natspecs, src, "inline/FuzzInlineConf.t.sol:FuzzInlineConf", "FuzzInlineConf");
862 assert_data_eq!(
863 format!("{natspecs:#?}"),
864 str![[r#"
865[
866 NatSpec {
867 contract: "inline/FuzzInlineConf.t.sol:FuzzInlineConf",
868 function: None,
869 line: "7:1",
870 docs: "forge-config: default.fuzz.runs = 1",
871 },
872 NatSpec {
873 contract: "inline/FuzzInlineConf.t.sol:FuzzInlineConf",
874 function: Some(
875 "testInlineConfFuzz1",
876 ),
877 line: "9:5",
878 docs: "forge-config: default.fuzz.runs = 3",
879 },
880]
881"#]]
882 );
883 }
884
885 #[test]
886 fn translates_legacy_halmos_array_lengths() {
887 let natspec = NatSpec {
888 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
889 function: Some("checkBytes".to_string()),
890 line: "10:1".to_string(),
891 docs: "@custom:halmos --loop 256 --array-lengths 2,4,8 --depth 100".to_string(),
892 };
893
894 assert_eq!(
895 natspec.halmos_config_values().unwrap(),
896 vec![
897 "default.symbolic.loop = 256",
898 "default.symbolic.array_lengths = [2, 4, 8]",
899 "default.symbolic.depth = 100",
900 ]
901 );
902 }
903
904 #[test]
905 fn translates_named_halmos_array_lengths() {
906 let natspec = NatSpec {
907 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
908 function: Some("checkBytes".to_string()),
909 line: "10:1".to_string(),
910 docs: "@custom:halmos --array-lengths values={2,4},data=8".to_string(),
911 };
912
913 assert_eq!(
914 natspec.halmos_config_values().unwrap(),
915 vec!["default.symbolic.dynamic_lengths = { data = [8], values = [2, 4] }"]
916 );
917 }
918
919 #[test]
920 fn translates_halmos_default_dynamic_length_sets() {
921 let natspec = NatSpec {
922 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
923 function: Some("checkBytes".to_string()),
924 line: "10:1".to_string(),
925 docs:
926 "@custom:halmos --default-array-lengths 0,1,2 --default-bytes-lengths={0,65,1024}"
927 .to_string(),
928 };
929
930 assert_eq!(
931 natspec.halmos_config_values().unwrap(),
932 vec![
933 "default.symbolic.default_array_lengths = [0, 1, 2]",
934 "default.symbolic.default_bytes_lengths = [0, 65, 1024]",
935 ]
936 );
937 }
938
939 #[test]
940 fn translates_legacy_halmos_width_depth_and_solver_timeout() {
941 let natspec = NatSpec {
942 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
943 function: Some("invariant_state".to_string()),
944 line: "10:1".to_string(),
945 docs: "@custom:halmos --width=32 --depth 128 --solver-timeout-branching 5".to_string(),
946 };
947
948 assert_eq!(
949 natspec.halmos_config_values().unwrap(),
950 vec![
951 "default.symbolic.width = 32",
952 "default.symbolic.depth = 128",
953 "default.symbolic.timeout = 5",
954 ]
955 );
956 }
957
958 #[test]
959 fn translates_legacy_halmos_solver_selection() {
960 let natspec = NatSpec {
961 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
962 function: Some("check_solver".to_string()),
963 line: "10:1".to_string(),
964 docs: "@custom:halmos --solver cvc5 --solver-command \"bitwuzla --produce-models\""
965 .to_string(),
966 };
967
968 assert_eq!(
969 natspec.halmos_config_values().unwrap(),
970 vec![
971 "default.symbolic.solver = \"cvc5\"",
972 "default.symbolic.solver_command = \"bitwuzla --produce-models\"",
973 ]
974 );
975 }
976
977 #[test]
978 fn rejects_malformed_legacy_halmos_array_lengths() {
979 let natspec = NatSpec {
980 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
981 function: Some("checkBytes".to_string()),
982 line: "10:1".to_string(),
983 docs: "@custom:halmos --array-lengths nope".to_string(),
984 };
985
986 let err = natspec.halmos_config_values().unwrap_err();
987
988 assert!(err.to_string().contains("invalid @custom:halmos annotation"));
989 assert!(err.to_string().contains("invalid length `nope`"));
990 }
991
992 #[test]
993 fn parse_solar_legacy_halmos_only_config() {
994 let src = r#"
995contract SymbolicHalmosLengths {
996 /// @custom:halmos --array-lengths 3
997 function checkArray(uint256[] memory values) public pure {
998 values;
999 }
1000}
1001 "#;
1002 let mut natspecs = vec![];
1003 parse(
1004 &mut natspecs,
1005 src,
1006 "inline/SymbolicHalmosLengths.t.sol:SymbolicHalmosLengths",
1007 "SymbolicHalmosLengths",
1008 );
1009
1010 assert_eq!(natspecs.len(), 1);
1011 assert_eq!(
1012 natspecs[0].halmos_config_values().unwrap(),
1013 vec!["default.symbolic.array_lengths = [3]"]
1014 );
1015 }
1016
1017 #[test]
1018 fn split_halmos_args_rejects_unterminated_quote() {
1019 let err = split_halmos_args(r#"--width "unterm"#).unwrap_err();
1020 assert_eq!(err, r#"unterminated " quote in @custom:halmos config"#);
1021 }
1022}