@@ -78,10 +78,10 @@ impl<'a> ParserContext<'a> {
7878
7979 match primary. as_rule ( ) {
8080 Rule :: integer => {
81- let int_str = primary. as_str ( ) ;
82- let int_value = int_str . parse :: < i32 > ( ) . unwrap ( ) ;
83- let bitvec = BitVecValue :: from_u64 ( int_value as u64 , 64 ) ;
84- Ok ( BoxedExpr :: Const ( bitvec , start, end) )
81+ let int_value = primary. as_str ( ) . parse :: < u64 > ( ) . unwrap ( ) ;
82+ let bvv = BitVecValue :: from_u64 ( int_value as u64 , 64 ) ;
83+
84+ Ok ( BoxedExpr :: Const ( bvv , start, end) )
8585 }
8686 Rule :: path_id => {
8787 let path_id = primary. as_str ( ) ;
@@ -290,9 +290,25 @@ impl<'a> ParserContext<'a> {
290290 while let Some ( inner_pair) = stmt_pairs. next ( ) {
291291 let start = inner_pair. as_span ( ) . start ( ) ;
292292 let end = inner_pair. as_span ( ) . end ( ) ;
293+
294+ // special case for step() -- will return a vector of statements
295+ if inner_pair. as_rule ( ) == Rule :: step {
296+ let step_stmt = self . parse_step ( inner_pair) ?;
297+
298+ // push each step statement into the transaction
299+ for step in step_stmt {
300+ let step_id = self . tr . s ( step) ;
301+ self . tr . add_stmt_loc ( step_id, start, end, self . fileid ) ;
302+ stmts. push ( step_id) ;
303+ }
304+
305+ continue ;
306+ }
307+
308+ // Handle other statement types
293309 let stmt = match inner_pair. as_rule ( ) {
294310 Rule :: assign => self . parse_assign ( inner_pair) ?,
295- Rule :: cmd => self . parse_cmd ( inner_pair) ?,
311+ Rule :: fork => self . parse_fork ( inner_pair) ?,
296312 Rule :: while_loop => self . parse_while ( inner_pair) ?,
297313 Rule :: cond => self . parse_cond ( inner_pair) ?,
298314 Rule :: assert_eq => self . parse_assert_eq ( inner_pair) ?,
@@ -310,6 +326,7 @@ impl<'a> ParserContext<'a> {
310326 return Err ( msg) ;
311327 }
312328 } ;
329+
313330 let stmt_id = self . tr . s ( stmt) ;
314331 self . tr . add_stmt_loc ( stmt_id, start, end, self . fileid ) ;
315332 stmts. push ( stmt_id) ;
@@ -338,52 +355,38 @@ impl<'a> ParserContext<'a> {
338355 Ok ( Stmt :: Assign ( symbol_id, expr_id) )
339356 }
340357
341- fn parse_cmd ( & mut self , pair : pest:: iterators:: Pair < Rule > ) -> Result < Stmt , String > {
358+ fn parse_step ( & mut self , pair : pest:: iterators:: Pair < Rule > ) -> Result < Vec < Stmt > , String > {
342359 let mut inner_rules = pair. clone ( ) . into_inner ( ) ;
343- let cmd_rule = self . expect_rule ( inner_rules. next ( ) , & pair, "Expected command" ) ?;
344- let cmd = cmd_rule. as_str ( ) ;
345-
346- let arg = if let Some ( expr_rule) = inner_rules. next ( ) {
347- let expr_id = self . parse_expr ( expr_rule. into_inner ( ) ) ?;
348- Some ( expr_id)
349- } else {
350- None
360+ let integer_rule = inner_rules. next ( ) ;
361+ let num_steps = match integer_rule {
362+ Some ( rule) => rule. as_str ( ) . parse :: < u64 > ( ) . unwrap ( ) ,
363+ None => 1 , // Implicit 1 if no integer is passed
351364 } ;
352365
353- match cmd {
354- "step" => match arg {
355- Some ( expr_id) => Ok ( Stmt :: Step ( expr_id) ) ,
356- None => {
357- let one_expr = self . tr . e ( Expr :: Const ( BitVecValue :: from_i64 ( 1 , 2 ) ) ) ;
358- self . handler . emit_diagnostic_parsing (
359- "Inferring step value to be 1." ,
360- self . fileid ,
361- & pair,
362- Level :: Warning ,
363- ) ;
364- Ok ( Stmt :: Step ( one_expr) )
365- }
366- } ,
367- "fork" => {
368- if arg. is_some ( ) {
369- let msg = "Fork command should have no arguments." . to_string ( ) ;
370- self . handler . emit_diagnostic_parsing (
371- & msg,
372- self . fileid ,
373- & cmd_rule,
374- Level :: Error ,
375- ) ;
376- return Err ( msg) ;
377- }
378- Ok ( Stmt :: Fork )
379- }
380- _ => {
381- let msg = format ! ( "Unexpected command: {:?}" , cmd) ;
382- self . handler
383- . emit_diagnostic_parsing ( & msg, self . fileid , & cmd_rule, Level :: Error ) ;
384- Err ( msg)
385- }
366+ // error if num_steps is 0 (note that the integer_rule is already unsigned, preventing negatives)
367+ if num_steps == 0 {
368+ let msg = format ! (
369+ "Step call expected single positive integer as argument, got {}." ,
370+ num_steps
371+ ) ;
372+ self . handler
373+ . emit_diagnostic_parsing ( & msg, self . fileid , & pair, Level :: Error ) ;
374+ return Err ( msg) ;
375+ }
376+
377+ // return a vector of steps based on num_steps
378+ let mut steps = Vec :: new ( ) ;
379+ for _ in 0 ..num_steps {
380+ let step_stmt = Stmt :: Step ;
381+ steps. push ( step_stmt) ;
386382 }
383+
384+ Ok ( steps)
385+ }
386+
387+ fn parse_fork ( & mut self , _pair : pest:: iterators:: Pair < Rule > ) -> Result < Stmt , String > {
388+ // Fork is a special case, it doesn't have any arguments (enforced by the grammar)
389+ Ok ( Stmt :: Fork )
387390 }
388391
389392 fn parse_while ( & mut self , pair : pest:: iterators:: Pair < Rule > ) -> Result < Stmt , String > {
0 commit comments