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 let value = value
244 .parse::<u32>()
245 .map_err(|_| format!("invalid value `{value}` for {}", arg.flag))?;
246 values.push(format!("default.symbolic.{} = {value}", arg.foundry_field));
247 Ok(())
248 }
249 HalmosArgParser::String => {
250 values.push(format!("default.symbolic.{} = {}", arg.foundry_field, toml_string(value)));
251 Ok(())
252 }
253 }
254}
255
256fn push_halmos_array_lengths(values: &mut Vec<String>, value: &str) -> Result<(), String> {
257 match parse_halmos_array_lengths(value)? {
258 HalmosArrayLengths::Positional(lengths) => {
259 values.push(format!(
260 "default.symbolic.array_lengths = [{}]",
261 lengths.iter().format(", ")
262 ));
263 }
264 HalmosArrayLengths::Named(lengths) => {
265 values.push(format!(
266 "default.symbolic.dynamic_lengths = {{ {} }}",
267 lengths
268 .iter()
269 .map(|(name, lengths)| format!("{name} = [{}]", lengths.iter().format(", ")))
270 .format(", ")
271 ));
272 }
273 }
274 Ok(())
275}
276
277fn push_halmos_lengths(
278 values: &mut Vec<String>,
279 field: &str,
280 value: &str,
281 flag: &str,
282) -> Result<(), String> {
283 values.push(format!(
284 "default.symbolic.{field} = [{}]",
285 parse_halmos_lengths(value, flag)?.iter().format(", ")
286 ));
287 Ok(())
288}
289
290fn toml_string(value: &str) -> String {
291 format!("\"{}\"", value.replace('\\', "\\\\").replace('"', "\\\""))
292}
293
294enum HalmosArrayLengths {
295 Positional(Vec<u32>),
296 Named(BTreeMap<String, Vec<u32>>),
297}
298
299fn parse_halmos_array_lengths(value: &str) -> Result<HalmosArrayLengths, String> {
300 if value.contains('=') {
301 let mut named = BTreeMap::new();
302 for entry in split_halmos_lengths_entries(value)? {
303 let Some((name, lengths)) = entry.split_once('=') else {
304 return Err(format!(
305 "mixed named and positional lengths in --array-lengths `{value}`"
306 ));
307 };
308 let name = name.trim();
309 if name.is_empty() {
310 return Err(format!("missing name in --array-lengths `{value}`"));
311 }
312 named
313 .insert(name.to_string(), parse_halmos_lengths(lengths.trim(), "--array-lengths")?);
314 }
315 if named.is_empty() {
316 return Err("missing value for --array-lengths".to_string());
317 }
318 Ok(HalmosArrayLengths::Named(named))
319 } else {
320 Ok(HalmosArrayLengths::Positional(parse_halmos_lengths(value, "--array-lengths")?))
321 }
322}
323
324fn parse_halmos_lengths(value: &str, flag: &str) -> Result<Vec<u32>, String> {
325 parse_halmos_length_set(value, flag)
326}
327
328fn parse_halmos_length_set(value: &str, flag: &str) -> Result<Vec<u32>, String> {
329 let value = value.trim();
330 let value = value.strip_prefix('{').and_then(|value| value.strip_suffix('}')).unwrap_or(value);
331 let mut lengths = Vec::new();
332 for length in value.split(',') {
333 let length = length.trim();
334 if length.is_empty() {
335 return Err(format!("invalid empty length in {flag} `{value}`"));
336 }
337 let length = length
338 .parse::<u32>()
339 .map_err(|_| format!("invalid length `{length}` in {flag} `{value}`"))?;
340 lengths.push(length);
341 }
342 if lengths.is_empty() {
343 return Err(format!("missing value for {flag}"));
344 }
345 Ok(lengths)
346}
347
348fn split_halmos_lengths_entries(value: &str) -> Result<Vec<&str>, String> {
349 let mut entries = Vec::new();
350 let mut start = 0usize;
351 let mut brace_depth = 0u8;
352 for (idx, ch) in value.char_indices() {
353 match ch {
354 '{' => brace_depth = brace_depth.saturating_add(1),
355 '}' => {
356 brace_depth = brace_depth
357 .checked_sub(1)
358 .ok_or_else(|| format!("unmatched `}}` in --array-lengths `{value}`"))?;
359 }
360 ',' if brace_depth == 0 => {
361 entries.push(value[start..idx].trim());
362 start = idx + 1;
363 }
364 _ => {}
365 }
366 }
367 if brace_depth != 0 {
368 return Err(format!("unmatched `{{` in --array-lengths `{value}`"));
369 }
370 entries.push(value[start..].trim());
371 Ok(entries)
372}
373
374struct SolcParser {
375 _private: (),
376}
377
378impl SolcParser {
379 const fn new() -> Self {
380 Self { _private: () }
381 }
382
383 fn contract_root_node<'a>(&self, nodes: &'a [Node], contract_id: &str) -> Option<&'a Node> {
386 for n in nodes {
387 if n.node_type == NodeType::ContractDefinition {
388 let contract_data = &n.other;
389 if let Value::String(contract_name) = contract_data.get("name")?
390 && contract_id.ends_with(contract_name)
391 {
392 return Some(n);
393 }
394 }
395 }
396 None
397 }
398
399 fn parse(&self, natspecs: &mut Vec<NatSpec>, contract: &str, node: &Node, root: bool) {
402 if root && let Some((docs, line)) = self.get_node_docs(&node.other) {
404 natspecs.push(NatSpec { contract: contract.into(), function: None, docs, line })
405 }
406 for n in &node.nodes {
407 if let Some((function, docs, line)) = self.get_fn_data(n) {
408 natspecs.push(NatSpec {
409 contract: contract.into(),
410 function: Some(function),
411 line,
412 docs,
413 })
414 }
415 self.parse(natspecs, contract, n, false);
416 }
417 }
418
419 fn get_fn_data(&self, node: &Node) -> Option<(String, String, String)> {
427 if node.node_type == NodeType::FunctionDefinition {
428 let fn_data = &node.other;
429 let fn_name: String = self.get_fn_name(fn_data)?;
430 let (fn_docs, docs_src_line) = self.get_node_docs(fn_data)?;
431 return Some((fn_name, fn_docs, docs_src_line));
432 }
433
434 None
435 }
436
437 fn get_fn_name(&self, fn_data: &BTreeMap<String, Value>) -> Option<String> {
439 match fn_data.get("name")? {
440 Value::String(fn_name) => Some(fn_name.into()),
441 _ => None,
442 }
443 }
444
445 fn get_node_docs(&self, data: &BTreeMap<String, Value>) -> Option<(String, String)> {
451 if let Value::Object(fn_docs) = data.get("documentation")?
452 && let Value::String(comment) = fn_docs.get("text")?
453 && contains_inline_config(comment)
454 {
455 let mut src_line = fn_docs
456 .get("src")
457 .map(|src| src.to_string())
458 .unwrap_or_else(|| String::from("<no-src-line-available>"));
459
460 src_line.retain(|c| c != '"');
461 return Some((comment.into(), src_line));
462 }
463 None
464 }
465}
466
467struct SolarParser<'a> {
468 sess: &'a Session,
469}
470
471impl<'a> SolarParser<'a> {
472 const fn new(sess: &'a Session) -> Self {
473 Self { sess }
474 }
475
476 fn parse_ast(
477 &self,
478 natspecs: &mut Vec<NatSpec>,
479 source_unit: &ast::SourceUnit<'_>,
480 contract_id: &str,
481 contract_name: &str,
482 ) {
483 let mut handle_docs = |item: &ast::Item<'_>| {
484 if item.docs.is_empty() {
485 return;
486 }
487 let mut span = Span::DUMMY;
488 let lines = item
489 .docs
490 .iter()
491 .filter_map(|d| {
492 let s = d.symbol.as_str();
493 if !contains_inline_config(s) {
494 return None;
495 }
496 span = if span.is_dummy() { d.span } else { span.to(d.span) };
497 match d.kind {
498 ast::CommentKind::Line => Some(s.trim().to_string()),
499 ast::CommentKind::Block => Some(
500 s.lines()
501 .filter(|line| contains_inline_config(line))
502 .map(|line| line.trim_start().trim_start_matches('*').trim())
503 .collect::<Vec<_>>()
504 .join("\n"),
505 ),
506 }
507 })
508 .join("\n");
509 if lines.is_empty() {
510 return;
511 }
512 natspecs.push(NatSpec {
513 contract: contract_id.to_string(),
514 function: if let ast::ItemKind::Function(f) = &item.kind {
515 Some(
516 f.header
517 .name
518 .map(|sym| sym.to_string())
519 .unwrap_or_else(|| f.kind.to_string()),
520 )
521 } else {
522 None
523 },
524 line: {
525 let (_, loc) = self.sess.source_map().span_to_location_info(span);
526 format!("{}:{}", loc.lo.line, loc.lo.col.0 + 1)
527 },
528 docs: lines,
529 });
530 };
531
532 for item in source_unit.items.iter() {
533 let ast::ItemKind::Contract(c) = &item.kind else { continue };
534 if c.name.as_str() != contract_name {
535 continue;
536 }
537
538 handle_docs(item);
540
541 for item in c.body.iter() {
543 let ast::ItemKind::Function(_) = &item.kind else { continue };
544 handle_docs(item);
545 }
546 }
547 }
548}
549
550fn contains_inline_config(s: &str) -> bool {
551 s.contains(INLINE_CONFIG_PREFIX) || s.contains(HALMOS_CONFIG_PREFIX)
552}
553
554#[cfg(test)]
555mod tests {
556 use super::*;
557 use serde_json::json;
558 use snapbox::{assert_data_eq, str};
559 use solar::parse::{
560 Parser,
561 ast::{Arena, interface},
562 };
563
564 fn parse(natspecs: &mut Vec<NatSpec>, src: &str, contract_id: &str, contract_name: &str) {
565 if !contains_inline_config(src) {
567 return;
568 }
569
570 let sess = Session::builder()
571 .with_silent_emitter(Some("Inline config parsing failed".to_string()))
572 .build();
573 let solar = SolarParser::new(&sess);
574 let _ = sess.enter(|| -> interface::Result<()> {
575 let arena = Arena::new();
576
577 let mut parser = Parser::from_source_code(
578 &sess,
579 &arena,
580 interface::source_map::FileName::Custom(contract_id.to_string()),
581 src.to_string(),
582 )?;
583
584 let source_unit = parser.parse_file().map_err(|e| e.emit())?;
585
586 solar.parse_ast(natspecs, &source_unit, contract_id, contract_name);
587
588 Ok(())
589 });
590 }
591
592 #[test]
593 fn can_reject_invalid_profiles() {
594 let profiles = ["ci".into(), "default".into()];
595 let natspec = NatSpec {
596 contract: Default::default(),
597 function: Default::default(),
598 line: Default::default(),
599 docs: r"
600 forge-config: ciii.invariant.depth = 1
601 forge-config: default.invariant.depth = 1
602 "
603 .into(),
604 };
605
606 let result = natspec.validate_profiles(&profiles);
607 assert!(result.is_err());
608 }
609
610 #[test]
611 fn can_accept_valid_profiles() {
612 let profiles = ["ci".into(), "default".into()];
613 let natspec = NatSpec {
614 contract: Default::default(),
615 function: Default::default(),
616 line: Default::default(),
617 docs: r"
618 forge-config: ci.invariant.depth = 1
619 forge-config: default.invariant.depth = 1
620 "
621 .into(),
622 };
623
624 let result = natspec.validate_profiles(&profiles);
625 assert!(result.is_ok());
626 }
627
628 #[test]
629 fn parse_solar() {
630 let src = "
631contract C { /// forge-config: default.fuzz.runs = 600
632
633\t\t\t\t /// forge-config: default.fuzz.runs = 601
634
635 function f1() {}
636 /** forge-config: default.fuzz.runs = 700 */
637function f2() {} /** forge-config: default.fuzz.runs = 800 */ function f3() {}
638
639/**
640 * forge-config: default.fuzz.runs = 1024
641 * forge-config: default.fuzz.max-test-rejects = 500
642 */
643 function f4() {}
644}
645";
646 let mut natspecs = vec![];
647 parse(&mut natspecs, src, "path.sol:C", "C");
648 assert_data_eq!(
649 format!("{natspecs:#?}"),
650 str![[r#"
651[
652 NatSpec {
653 contract: "path.sol:C",
654 function: Some(
655 "f1",
656 ),
657 line: "2:14",
658 docs: "forge-config: default.fuzz.runs = 600/nforge-config: default.fuzz.runs = 601",
659 },
660 NatSpec {
661 contract: "path.sol:C",
662 function: Some(
663 "f2",
664 ),
665 line: "7:8",
666 docs: "forge-config: default.fuzz.runs = 700",
667 },
668 NatSpec {
669 contract: "path.sol:C",
670 function: Some(
671 "f3",
672 ),
673 line: "8:18",
674 docs: "forge-config: default.fuzz.runs = 800",
675 },
676 NatSpec {
677 contract: "path.sol:C",
678 function: Some(
679 "f4",
680 ),
681 line: "10:1",
682 docs: "forge-config: default.fuzz.runs = 1024/nforge-config: default.fuzz.max-test-rejects = 500",
683 },
684]
685"#]]
686 );
687 }
688
689 #[test]
690 fn parse_solar_2() {
691 let src = r#"
692// SPDX-License-Identifier: MIT OR Apache-2.0
693pragma solidity >=0.8.0;
694
695import "ds-test/test.sol";
696
697contract FuzzInlineConf is DSTest {
698 /**
699 * forge-config: default.fuzz.runs = 1024
700 * forge-config: default.fuzz.max-test-rejects = 500
701 */
702 function testInlineConfFuzz(uint8 x) public {
703 require(true, "this is not going to revert");
704 }
705}
706 "#;
707 let mut natspecs = vec![];
708 parse(&mut natspecs, src, "inline/FuzzInlineConf.t.sol:FuzzInlineConf", "FuzzInlineConf");
709 assert_data_eq!(
710 format!("{natspecs:#?}"),
711 str![[r#"
712[
713 NatSpec {
714 contract: "inline/FuzzInlineConf.t.sol:FuzzInlineConf",
715 function: Some(
716 "testInlineConfFuzz",
717 ),
718 line: "8:5",
719 docs: "forge-config: default.fuzz.runs = 1024/nforge-config: default.fuzz.max-test-rejects = 500",
720 },
721]
722"#]]
723 );
724 }
725
726 #[test]
727 fn config_lines() {
728 let natspec = natspec();
729 let config_lines = natspec.config_values();
730 assert_eq!(
731 config_lines.collect::<Vec<_>>(),
732 [
733 "default.fuzz.runs = 600".to_string(),
734 "ci.fuzz.runs = 500".to_string(),
735 "default.invariant.runs = 1".to_string()
736 ]
737 )
738 }
739
740 #[test]
741 fn can_handle_unavailable_src_line_with_fallback() {
742 let mut fn_data: BTreeMap<String, Value> = BTreeMap::new();
743 let doc_without_src_field = json!({ "text": "forge-config:default.fuzz.runs=600" });
744 fn_data.insert("documentation".into(), doc_without_src_field);
745 let (_, src_line) = SolcParser::new().get_node_docs(&fn_data).expect("Some docs");
746 assert_eq!(src_line, "<no-src-line-available>".to_string());
747 }
748
749 #[test]
750 fn can_handle_available_src_line() {
751 let mut fn_data: BTreeMap<String, Value> = BTreeMap::new();
752 let doc_without_src_field =
753 json!({ "text": "forge-config:default.fuzz.runs=600", "src": "73:21:12" });
754 fn_data.insert("documentation".into(), doc_without_src_field);
755 let (_, src_line) = SolcParser::new().get_node_docs(&fn_data).expect("Some docs");
756 assert_eq!(src_line, "73:21:12".to_string());
757 }
758
759 fn natspec() -> NatSpec {
760 let conf = r"
761 forge-config: default.fuzz.runs = 600
762 forge-config: ci.fuzz.runs = 500
763 ========= SOME NOISY TEXT =============
764 䩹𧀫Jx닧Ʀ̳盅K擷Ɂw첊}ꏻk86ᖪk-檻ܴ렝[Dz𐤬oᘓƤ
765 ꣖ۻ%Ƅ㪕ς:(饁av/烲ڻ̛߉橞㗡𥺃̹M봓䀖ؿ̄)d
766 ϊ&»ϿЏ2鞷砕eߥHJ粊머?槿ᴴጅϖ뀓Ӽ츙4
767 醤㭊r ܖ̹灱녗V*竅⒪苏贗=숽ؓбݧʹ園Ьi
768 =======================================
769 forge-config: default.invariant.runs = 1
770 ";
771
772 NatSpec {
773 contract: "dir/TestContract.t.sol:FuzzContract".to_string(),
774 function: Some("test_myFunction".to_string()),
775 line: "10:12:111".to_string(),
776 docs: conf.to_string(),
777 }
778 }
779
780 #[test]
781 fn parse_solar_multiple_contracts_from_same_file() {
782 let src = r#"
783// SPDX-License-Identifier: MIT OR Apache-2.0
784pragma solidity >=0.8.0;
785
786import "ds-test/test.sol";
787
788contract FuzzInlineConf is DSTest {
789 /// forge-config: default.fuzz.runs = 1
790 function testInlineConfFuzz1() {}
791}
792
793contract FuzzInlineConf2 is DSTest {
794 /// forge-config: default.fuzz.runs = 2
795 function testInlineConfFuzz2() {}
796}
797 "#;
798 let mut natspecs = vec![];
799 parse(&mut natspecs, src, "inline/FuzzInlineConf.t.sol:FuzzInlineConf", "FuzzInlineConf");
800 assert_data_eq!(
801 format!("{natspecs:#?}"),
802 str![[r#"
803[
804 NatSpec {
805 contract: "inline/FuzzInlineConf.t.sol:FuzzInlineConf",
806 function: Some(
807 "testInlineConfFuzz1",
808 ),
809 line: "8:6",
810 docs: "forge-config: default.fuzz.runs = 1",
811 },
812]
813"#]]
814 );
815
816 let mut natspecs = vec![];
817 parse(
818 &mut natspecs,
819 src,
820 "inline/FuzzInlineConf2.t.sol:FuzzInlineConf2",
821 "FuzzInlineConf2",
822 );
823 assert_data_eq!(
824 format!("{natspecs:#?}"),
825 str![[r#"
826[
827 NatSpec {
828 contract: "inline/FuzzInlineConf2.t.sol:FuzzInlineConf2",
829 function: Some(
830 "testInlineConfFuzz2",
831 ),
832 line: "13:5",
833 docs: "forge-config: default.fuzz.runs = 2",
834 },
835]
836"#]]
837 );
838 }
839
840 #[test]
841 fn parse_contract_level_config() {
842 let src = r#"
843// SPDX-License-Identifier: MIT OR Apache-2.0
844pragma solidity >=0.8.0;
845
846import "ds-test/test.sol";
847
848/// forge-config: default.fuzz.runs = 1
849contract FuzzInlineConf is DSTest {
850 /// forge-config: default.fuzz.runs = 3
851 function testInlineConfFuzz1() {}
852
853 function testInlineConfFuzz2() {}
854}"#;
855 let mut natspecs = vec![];
856 parse(&mut natspecs, src, "inline/FuzzInlineConf.t.sol:FuzzInlineConf", "FuzzInlineConf");
857 assert_data_eq!(
858 format!("{natspecs:#?}"),
859 str![[r#"
860[
861 NatSpec {
862 contract: "inline/FuzzInlineConf.t.sol:FuzzInlineConf",
863 function: None,
864 line: "7:1",
865 docs: "forge-config: default.fuzz.runs = 1",
866 },
867 NatSpec {
868 contract: "inline/FuzzInlineConf.t.sol:FuzzInlineConf",
869 function: Some(
870 "testInlineConfFuzz1",
871 ),
872 line: "9:5",
873 docs: "forge-config: default.fuzz.runs = 3",
874 },
875]
876"#]]
877 );
878 }
879
880 #[test]
881 fn translates_legacy_halmos_array_lengths() {
882 let natspec = NatSpec {
883 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
884 function: Some("checkBytes".to_string()),
885 line: "10:1".to_string(),
886 docs: "@custom:halmos --loop 256 --array-lengths 2,4,8 --depth 100".to_string(),
887 };
888
889 assert_eq!(
890 natspec.halmos_config_values().unwrap(),
891 vec![
892 "default.symbolic.loop = 256",
893 "default.symbolic.array_lengths = [2, 4, 8]",
894 "default.symbolic.depth = 100",
895 ]
896 );
897 }
898
899 #[test]
900 fn translates_named_halmos_array_lengths() {
901 let natspec = NatSpec {
902 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
903 function: Some("checkBytes".to_string()),
904 line: "10:1".to_string(),
905 docs: "@custom:halmos --array-lengths values={2,4},data=8".to_string(),
906 };
907
908 assert_eq!(
909 natspec.halmos_config_values().unwrap(),
910 vec!["default.symbolic.dynamic_lengths = { data = [8], values = [2, 4] }"]
911 );
912 }
913
914 #[test]
915 fn translates_halmos_default_dynamic_length_sets() {
916 let natspec = NatSpec {
917 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
918 function: Some("checkBytes".to_string()),
919 line: "10:1".to_string(),
920 docs:
921 "@custom:halmos --default-array-lengths 0,1,2 --default-bytes-lengths={0,65,1024}"
922 .to_string(),
923 };
924
925 assert_eq!(
926 natspec.halmos_config_values().unwrap(),
927 vec![
928 "default.symbolic.default_array_lengths = [0, 1, 2]",
929 "default.symbolic.default_bytes_lengths = [0, 65, 1024]",
930 ]
931 );
932 }
933
934 #[test]
935 fn translates_legacy_halmos_width_depth_and_solver_timeout() {
936 let natspec = NatSpec {
937 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
938 function: Some("invariant_state".to_string()),
939 line: "10:1".to_string(),
940 docs: "@custom:halmos --width=32 --depth 128 --solver-timeout-branching 5".to_string(),
941 };
942
943 assert_eq!(
944 natspec.halmos_config_values().unwrap(),
945 vec![
946 "default.symbolic.width = 32",
947 "default.symbolic.depth = 128",
948 "default.symbolic.timeout = 5",
949 ]
950 );
951 }
952
953 #[test]
954 fn translates_legacy_halmos_solver_selection() {
955 let natspec = NatSpec {
956 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
957 function: Some("check_solver".to_string()),
958 line: "10:1".to_string(),
959 docs: "@custom:halmos --solver cvc5 --solver-command \"bitwuzla --produce-models\""
960 .to_string(),
961 };
962
963 assert_eq!(
964 natspec.halmos_config_values().unwrap(),
965 vec![
966 "default.symbolic.solver = \"cvc5\"",
967 "default.symbolic.solver_command = \"bitwuzla --produce-models\"",
968 ]
969 );
970 }
971
972 #[test]
973 fn rejects_malformed_legacy_halmos_array_lengths() {
974 let natspec = NatSpec {
975 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
976 function: Some("checkBytes".to_string()),
977 line: "10:1".to_string(),
978 docs: "@custom:halmos --array-lengths nope".to_string(),
979 };
980
981 let err = natspec.halmos_config_values().unwrap_err();
982
983 assert!(err.to_string().contains("invalid @custom:halmos annotation"));
984 assert!(err.to_string().contains("invalid length `nope`"));
985 }
986
987 #[test]
988 fn ignores_unsupported_halmos_flags_while_translating_supported_ones() {
989 let natspec = NatSpec {
990 contract: "dir/TestContract.t.sol:SymbolicContract".to_string(),
991 function: Some("checkBytes".to_string()),
992 line: "10:1".to_string(),
993 docs: "@custom:halmos --unsupported value --loop 10 --another --array-lengths 2"
994 .to_string(),
995 };
996
997 assert_eq!(
998 natspec.halmos_config_values().unwrap(),
999 vec!["default.symbolic.loop = 10", "default.symbolic.array_lengths = [2]",]
1000 );
1001 }
1002
1003 #[test]
1004 fn parse_solar_legacy_halmos_only_config() {
1005 let src = r#"
1006contract SymbolicHalmosLengths {
1007 /// @custom:halmos --array-lengths 3
1008 function checkArray(uint256[] memory values) public pure {
1009 values;
1010 }
1011}
1012 "#;
1013 let mut natspecs = vec![];
1014 parse(
1015 &mut natspecs,
1016 src,
1017 "inline/SymbolicHalmosLengths.t.sol:SymbolicHalmosLengths",
1018 "SymbolicHalmosLengths",
1019 );
1020
1021 assert_eq!(natspecs.len(), 1);
1022 assert_eq!(
1023 natspecs[0].halmos_config_values().unwrap(),
1024 vec!["default.symbolic.array_lengths = [3]"]
1025 );
1026 }
1027
1028 #[test]
1029 fn split_halmos_args_rejects_unterminated_quote() {
1030 let err = split_halmos_args(r#"--width "unterm"#).unwrap_err();
1031 assert_eq!(err, "invalid shell quoting in @custom:halmos config");
1032 }
1033}