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