@@ -3,7 +3,7 @@ use crate::{
33 ir:: HighLevelOperation ,
44 lang:: {
55 AssumeBoolean , Boolean , Condition , ConstExpression , ConstMallocLabel , ConstantValue , Expression , Function ,
6- Line , Program , SimpleExpr , Var ,
6+ Line , Program , SimpleExpr , Var , Context , Scope ,
77 } ,
88} ;
99use lean_vm:: { SourceLineNumber , Table , TableT } ;
@@ -72,6 +72,7 @@ pub enum SimpleLine {
7272 value : SimpleExpr ,
7373 arms : Vec < Vec < Self > > , // patterns = 0, 1, ...
7474 } ,
75+ ForwardDeclaration { var : Var } ,
7576 Assignment {
7677 var : VarOrConstMallocAccess ,
7778 operation : HighLevelOperation ,
@@ -150,6 +151,7 @@ pub enum SimpleLine {
150151}
151152
152153pub fn simplify_program ( mut program : Program ) -> SimpleProgram {
154+ check_program_scoping ( & program) ;
153155 handle_inlined_functions ( & mut program) ;
154156 handle_const_arguments ( & mut program) ;
155157 let mut new_functions = BTreeMap :: new ( ) ;
@@ -189,6 +191,168 @@ pub fn simplify_program(mut program: Program) -> SimpleProgram {
189191 }
190192}
191193
194+ /// Analyzes the program to verify that each variable is defined in each context where it is used.
195+ fn check_program_scoping ( program : & Program ) {
196+ for ( _, function) in program. functions . iter ( ) {
197+ let mut scope = Scope { vars : BTreeSet :: new ( ) } ;
198+ for ( arg, _) in function. arguments . iter ( ) {
199+ scope. vars . insert ( arg. clone ( ) ) ;
200+ }
201+ let mut ctx = Context { scopes : vec ! [ scope] } ;
202+
203+ check_block_scoping ( & function. body , & mut ctx) ;
204+ }
205+ }
206+
207+ /// Analyzes the block to verify that each variable is defined in each context where it is used.
208+ fn check_block_scoping ( block : & Vec < Line > , ctx : & mut Context ) {
209+ for line in block. iter ( ) {
210+ match line {
211+ Line :: ForwardDeclaration { var } => {
212+ let last_scope = ctx. scopes . last_mut ( ) . unwrap ( ) ;
213+ assert ! ( !last_scope. vars. contains( var) , "Variable declared multiple times in the same scope: {:?}" , var) ;
214+ last_scope. vars . insert ( var. clone ( ) ) ;
215+ } ,
216+ Line :: Match { value, arms } => {
217+ check_expr_scoping ( value, ctx) ;
218+ for ( _, arm) in arms {
219+ ctx. scopes . push ( Scope { vars : BTreeSet :: new ( ) } ) ;
220+ check_block_scoping ( arm, ctx) ;
221+ ctx. scopes . pop ( ) ;
222+ }
223+ } ,
224+ Line :: Assignment { var, value } => {
225+ check_expr_scoping ( value, ctx) ;
226+ let last_scope = ctx. scopes . last_mut ( ) . unwrap ( ) ;
227+ assert ! ( !last_scope. vars. contains( var) , "Variable declared multiple times in the same scope: {:?}" , var) ;
228+ last_scope. vars . insert ( var. clone ( ) ) ;
229+ } ,
230+ Line :: ArrayAssign { array, index, value } => {
231+ check_simple_expr_scoping ( array, ctx) ;
232+ check_expr_scoping ( index, ctx) ;
233+ check_expr_scoping ( value, ctx) ;
234+ } ,
235+ Line :: Assert ( boolean, _) => {
236+ check_boolean_scoping ( boolean, ctx) ;
237+ } ,
238+ Line :: IfCondition { condition, then_branch, else_branch, line_number : _ } => {
239+ check_condition_scoping ( condition, ctx) ;
240+ for branch in [ then_branch, else_branch] {
241+ ctx. scopes . push ( Scope { vars : BTreeSet :: new ( ) } ) ;
242+ check_block_scoping ( branch, ctx) ;
243+ ctx. scopes . pop ( ) ;
244+ }
245+ } ,
246+ Line :: ForLoop { iterator, start, end, body, rev : _, unroll : _, line_number : _ } => {
247+ check_expr_scoping ( start, ctx) ;
248+ check_expr_scoping ( end, ctx) ;
249+ let mut new_scope_vars = BTreeSet :: new ( ) ;
250+ new_scope_vars. insert ( iterator. clone ( ) ) ;
251+ ctx. scopes . push ( Scope { vars : new_scope_vars } ) ;
252+ check_block_scoping ( body, ctx) ;
253+ ctx. scopes . pop ( ) ;
254+ } ,
255+ Line :: FunctionCall { function_name : _, args, return_data, line_number : _ } => {
256+ for arg in args {
257+ check_expr_scoping ( arg, ctx) ;
258+ }
259+ let last_scope = ctx. scopes . last_mut ( ) . unwrap ( ) ;
260+ for var in return_data {
261+ assert ! ( !last_scope. vars. contains( var) , "Variable declared multiple times in the same scope: {:?}" , var) ;
262+ last_scope. vars . insert ( var. clone ( ) ) ;
263+ }
264+ } ,
265+ Line :: FunctionRet { return_data } => {
266+ for expr in return_data {
267+ check_expr_scoping ( expr, ctx) ;
268+ }
269+ } ,
270+ Line :: Precompile { table : _, args } => {
271+ for arg in args {
272+ check_expr_scoping ( arg, ctx) ;
273+ }
274+ } ,
275+ Line :: Break | Line :: Panic | Line :: LocationReport { .. } => { } ,
276+ Line :: Print { line_info : _, content } => {
277+ for expr in content {
278+ check_expr_scoping ( expr, ctx) ;
279+ }
280+ } ,
281+ Line :: MAlloc { var, size, vectorized : _, vectorized_len } => {
282+ check_expr_scoping ( size, ctx) ;
283+ check_expr_scoping ( vectorized_len, ctx) ;
284+ let last_scope = ctx. scopes . last_mut ( ) . unwrap ( ) ;
285+ assert ! ( !last_scope. vars. contains( var) , "Variable declared multiple times in the same scope: {:?}" , var) ;
286+ last_scope. vars . insert ( var. clone ( ) ) ;
287+ } ,
288+ Line :: DecomposeBits { var, to_decompose } | Line :: DecomposeCustom { var, to_decompose } => {
289+ for expr in to_decompose {
290+ check_expr_scoping ( expr, ctx) ;
291+ }
292+ let last_scope = ctx. scopes . last_mut ( ) . unwrap ( ) ;
293+ assert ! ( !last_scope. vars. contains( var) , "Variable declared multiple times in the same scope: {:?}" , var) ;
294+ last_scope. vars . insert ( var. clone ( ) ) ;
295+ } ,
296+ Line :: CounterHint { var } => {
297+ let last_scope = ctx. scopes . last_mut ( ) . unwrap ( ) ;
298+ assert ! ( !last_scope. vars. contains( var) , "Variable declared multiple times in the same scope: {:?}" , var) ;
299+ last_scope. vars . insert ( var. clone ( ) ) ;
300+ } ,
301+ }
302+ }
303+ }
304+
305+ /// Analyzes the expression to verify that each variable is defined in the given context.
306+ fn check_expr_scoping ( expr : & Expression , ctx : & Context ) {
307+ match expr {
308+ Expression :: Value ( simple_expr) => {
309+ check_simple_expr_scoping ( simple_expr, ctx) ;
310+ } ,
311+ Expression :: ArrayAccess { array, index } => {
312+ check_simple_expr_scoping ( array, ctx) ;
313+ check_expr_scoping ( & * index, ctx) ;
314+ } ,
315+ Expression :: Binary { left, operation : _, right } => {
316+ check_expr_scoping ( & * left, ctx) ;
317+ check_expr_scoping ( & * right, ctx) ;
318+ } ,
319+ Expression :: Log2Ceil { value } => {
320+ check_expr_scoping ( & * value, ctx) ;
321+ } ,
322+ }
323+ }
324+
325+ /// Analyzes the simple expression to verify that each variable is defined in the given context.
326+ fn check_simple_expr_scoping ( expr : & SimpleExpr , ctx : & Context ) {
327+ match expr {
328+ SimpleExpr :: Var ( v) => {
329+ assert ! ( ctx. defines( & v) , "Variable defined but not used: {:?}" , v)
330+ } ,
331+ SimpleExpr :: Constant ( _) => { } ,
332+ SimpleExpr :: ConstMallocAccess { .. } => { } ,
333+ }
334+ }
335+
336+ fn check_boolean_scoping ( boolean : & Boolean , ctx : & Context ) {
337+ match boolean {
338+ Boolean :: Equal { left, right } | Boolean :: Different { left, right } => {
339+ check_expr_scoping ( left, ctx) ;
340+ check_expr_scoping ( right, ctx) ;
341+ } ,
342+ }
343+ }
344+
345+ fn check_condition_scoping ( condition : & Condition , ctx : & Context ) {
346+ match condition {
347+ Condition :: Expression ( expr, _) => {
348+ check_expr_scoping ( expr, ctx) ;
349+ } ,
350+ Condition :: Comparison ( boolean) => {
351+ check_boolean_scoping ( boolean, ctx) ;
352+ }
353+ }
354+ }
355+
192356#[ derive( Debug , Clone , Default ) ]
193357struct Counters {
194358 aux_vars : usize ,
@@ -233,6 +397,9 @@ fn simplify_lines(
233397 let mut res = Vec :: new ( ) ;
234398 for line in lines {
235399 match line {
400+ Line :: ForwardDeclaration { var : _ } => {
401+ todo ! ( ) ;
402+ } ,
236403 Line :: Match { value, arms } => {
237404 let simple_value = simplify_expr ( value, & mut res, counters, array_manager, const_malloc) ;
238405 let mut simple_arms = vec ! [ ] ;
@@ -782,6 +949,10 @@ pub fn find_variable_usage(lines: &[Line]) -> (BTreeSet<Var>, BTreeSet<Var>) {
782949
783950 for line in lines {
784951 match line {
952+ Line :: ForwardDeclaration { var : _ } => {
953+ todo ! ( ) ;
954+ // internal_vars.push(var.clone()); // if declaring is using; otherwise do nothing
955+ } ,
785956 Line :: Match { value, arms } => {
786957 on_new_expr ( value, & internal_vars, & mut external_vars) ;
787958 for ( _, statements) in arms {
@@ -927,14 +1098,17 @@ pub fn inline_lines(lines: &mut Vec<Line>, args: &BTreeMap<Var, SimpleExpr>, res
9271098 let inline_internal_var = |var : & mut Var | {
9281099 assert ! (
9291100 !args. contains_key( var) ,
930- "Variable {var} is both an argument and assigned in the inlined function"
1101+ "Variable {var} is both an argument and declared in the inlined function"
9311102 ) ;
9321103 * var = format ! ( "@inlined_var_{inlining_count}_{var}" ) ;
9331104 } ;
9341105
9351106 let mut lines_to_replace = vec ! [ ] ;
9361107 for ( i, line) in lines. iter_mut ( ) . enumerate ( ) {
9371108 match line {
1109+ Line :: ForwardDeclaration { var } => {
1110+ inline_internal_var ( var) ;
1111+ }
9381112 Line :: Match { value, arms } => {
9391113 inline_expr ( value, args, inlining_count) ;
9401114 for ( _, statements) in arms {
@@ -1240,6 +1414,9 @@ fn replace_vars_for_unroll(
12401414 replace_vars_for_unroll ( statements, iterator, unroll_index, iterator_value, internal_vars) ;
12411415 }
12421416 }
1417+ Line :: ForwardDeclaration { var } => {
1418+ * var = format ! ( "@unrolled_{unroll_index}_{iterator_value}_{var}" ) ;
1419+ }
12431420 Line :: Assignment { var, value } => {
12441421 assert ! ( var != iterator, "Weird" ) ;
12451422 * var = format ! ( "@unrolled_{unroll_index}_{iterator_value}_{var}" ) ;
@@ -1689,6 +1866,7 @@ fn get_function_called(lines: &[Line], function_called: &mut Vec<String>) {
16891866 get_function_called ( body, function_called) ;
16901867 }
16911868 Line :: Assignment { .. }
1869+ | Line :: ForwardDeclaration { .. }
16921870 | Line :: ArrayAssign { .. }
16931871 | Line :: Assert { .. }
16941872 | Line :: FunctionRet { .. }
@@ -1714,6 +1892,9 @@ fn replace_vars_by_const_in_lines(lines: &mut [Line], map: &BTreeMap<Var, F>) {
17141892 replace_vars_by_const_in_lines ( statements, map) ;
17151893 }
17161894 }
1895+ Line :: ForwardDeclaration { var } => {
1896+ assert ! ( !map. contains_key( var) , "Variable {var} is a constant" ) ;
1897+ }
17171898 Line :: Assignment { var, value } => {
17181899 assert ! ( !map. contains_key( var) , "Variable {var} is a constant" ) ;
17191900 replace_vars_by_const_in_expr ( value, map) ;
0 commit comments