@@ -250,182 +250,200 @@ fn check_privileged_operations_on_structs(env: &GlobalEnv, fun_env: &FunctionEnv
250250 let caller_module_id = fun_env. module_env . get_id ( ) ;
251251 let caller_is_inline_non_private =
252252 fun_env. is_inline ( ) && fun_env. visibility ( ) != Visibility :: Private ;
253- fun_body. visit_pre_order ( & mut |exp : & ExpData | {
254- match exp {
255- ExpData :: Call ( id, oper, _) => match oper {
256- Operation :: Exists ( _)
257- | Operation :: BorrowGlobal ( _)
258- | Operation :: MoveFrom
259- | Operation :: MoveTo => {
260- let inst = env. get_node_instantiation ( * id) ;
261- debug_assert ! ( !inst. is_empty( ) ) ;
262- if let Some ( ( struct_env, _) ) = inst[ 0 ] . get_struct ( env) {
263- let mid = struct_env. module_env . get_id ( ) ;
264- let sid = struct_env. get_id ( ) ;
265- let qualified_struct_id = mid. qualified ( sid) ;
253+ // Ancestor spec blocks seen during AST traversal.
254+ let mut spec_blocks_seen = 0 ;
255+ fun_body. visit_pre_post ( & mut |post, exp : & ExpData | {
256+ if !post {
257+ if matches ! ( exp, ExpData :: SpecBlock ( ..) ) {
258+ spec_blocks_seen += 1 ;
259+ }
260+ if spec_blocks_seen > 0 {
261+ // we are inside a spec block, no privileged operation check needed
262+ return true ;
263+ }
264+ match exp {
265+ ExpData :: Call ( id, oper, _) => match oper {
266+ Operation :: Exists ( _)
267+ | Operation :: BorrowGlobal ( _)
268+ | Operation :: MoveFrom
269+ | Operation :: MoveTo => {
270+ let inst = env. get_node_instantiation ( * id) ;
271+ debug_assert ! ( !inst. is_empty( ) ) ;
272+ if let Some ( ( struct_env, _) ) = inst[ 0 ] . get_struct ( env) {
273+ let mid = struct_env. module_env . get_id ( ) ;
274+ let sid = struct_env. get_id ( ) ;
275+ let qualified_struct_id = mid. qualified ( sid) ;
276+ let struct_env = env. get_struct ( qualified_struct_id) ;
277+ let msg_maker = || {
278+ format ! (
279+ "storage operation on type `{}`" ,
280+ struct_env. get_full_name_str( ) ,
281+ )
282+ } ;
283+ check_for_access_error_or_warning (
284+ env,
285+ fun_env,
286+ id,
287+ "called" ,
288+ msg_maker,
289+ & struct_env. module_env ,
290+ mid != caller_module_id,
291+ caller_is_inline_non_private,
292+ ) ;
293+ }
294+ } ,
295+ Operation :: Select ( mid, sid, fid) => {
296+ let qualified_struct_id = mid. qualified ( * sid) ;
266297 let struct_env = env. get_struct ( qualified_struct_id) ;
267298 let msg_maker = || {
268299 format ! (
269- "storage operation on type `{}`" ,
300+ "access of the field `{}` on type `{}`" ,
301+ fid. symbol( ) . display( struct_env. symbol_pool( ) ) ,
270302 struct_env. get_full_name_str( ) ,
271303 )
272304 } ;
273305 check_for_access_error_or_warning (
274306 env,
275307 fun_env,
276308 id,
277- "called " ,
309+ "accessed " ,
278310 msg_maker,
279311 & struct_env. module_env ,
280- mid != caller_module_id,
312+ * mid != caller_module_id,
281313 caller_is_inline_non_private,
282314 ) ;
283- }
284- } ,
285- Operation :: Select ( mid, sid, fid) => {
286- let qualified_struct_id = mid. qualified ( * sid) ;
287- let struct_env = env. get_struct ( qualified_struct_id) ;
288- let msg_maker = || {
289- format ! (
290- "access of the field `{}` on type `{}`" ,
291- fid. symbol( ) . display( struct_env. symbol_pool( ) ) ,
292- struct_env. get_full_name_str( ) ,
293- )
294- } ;
295- check_for_access_error_or_warning (
296- env,
297- fun_env,
298- id,
299- "accessed" ,
300- msg_maker,
301- & struct_env. module_env ,
302- * mid != caller_module_id,
303- caller_is_inline_non_private,
304- ) ;
305- } ,
306- Operation :: SelectVariants ( mid, sid, fids) => {
307- let qualified_struct_id = mid. qualified ( * sid) ;
308- let struct_env = env. get_struct ( qualified_struct_id) ;
309- // All field names are the same, so take one representative field id to report.
310- let field_env = struct_env. get_field ( fids[ 0 ] ) ;
311- let msg_maker = || {
312- format ! (
313- "access of the field `{}` on enum type `{}`" ,
314- field_env. get_name( ) . display( struct_env. symbol_pool( ) ) ,
315- struct_env. get_full_name_str( ) ,
316- )
317- } ;
318- check_for_access_error_or_warning (
319- env,
320- fun_env,
321- id,
322- "accessed" ,
323- msg_maker,
324- & struct_env. module_env ,
325- * mid != caller_module_id,
326- caller_is_inline_non_private,
327- ) ;
328- } ,
329- Operation :: TestVariants ( mid, sid, _) => {
330- let qualified_struct_id = mid. qualified ( * sid) ;
331- let struct_env = env. get_struct ( qualified_struct_id) ;
332- let msg_maker = || {
333- format ! (
334- "variant test on enum type `{}`" ,
335- struct_env. get_full_name_str( ) ,
336- )
337- } ;
338- check_for_access_error_or_warning (
339- env,
340- fun_env,
341- id,
342- "tested" ,
343- msg_maker,
344- & struct_env. module_env ,
345- * mid != caller_module_id,
346- caller_is_inline_non_private,
347- ) ;
348- } ,
349- Operation :: Pack ( mid, sid, _) => {
350- let qualified_struct_id = mid. qualified ( * sid) ;
351- let struct_env = env. get_struct ( qualified_struct_id) ;
352- let msg_maker = || format ! ( "pack of `{}`" , struct_env. get_full_name_str( ) ) ;
353- check_for_access_error_or_warning (
354- env,
355- fun_env,
356- id,
357- "packed" ,
358- msg_maker,
359- & struct_env. module_env ,
360- * mid != caller_module_id,
361- caller_is_inline_non_private,
362- ) ;
363- } ,
364- _ => {
365- // all the other operations are either:
366- // - not related to structs
367- // - spec-only
368- } ,
369- } ,
370- ExpData :: Assign ( _, pat, _)
371- | ExpData :: Block ( _, pat, _, _)
372- | ExpData :: Lambda ( _, pat, _, _, _) => {
373- pat. visit_pre_post ( & mut |_, pat| {
374- if let Pattern :: Struct ( id, str, _, _) = pat {
375- let module_id = str. module_id ;
376- let struct_env = env. get_struct ( str. to_qualified_id ( ) ) ;
315+ } ,
316+ Operation :: SelectVariants ( mid, sid, fids) => {
317+ let qualified_struct_id = mid. qualified ( * sid) ;
318+ let struct_env = env. get_struct ( qualified_struct_id) ;
319+ // All field names are the same, so take one representative field id to report.
320+ let field_env = struct_env. get_field ( fids[ 0 ] ) ;
321+ let msg_maker = || {
322+ format ! (
323+ "access of the field `{}` on enum type `{}`" ,
324+ field_env. get_name( ) . display( struct_env. symbol_pool( ) ) ,
325+ struct_env. get_full_name_str( ) ,
326+ )
327+ } ;
328+ check_for_access_error_or_warning (
329+ env,
330+ fun_env,
331+ id,
332+ "accessed" ,
333+ msg_maker,
334+ & struct_env. module_env ,
335+ * mid != caller_module_id,
336+ caller_is_inline_non_private,
337+ ) ;
338+ } ,
339+ Operation :: TestVariants ( mid, sid, _) => {
340+ let qualified_struct_id = mid. qualified ( * sid) ;
341+ let struct_env = env. get_struct ( qualified_struct_id) ;
342+ let msg_maker = || {
343+ format ! (
344+ "variant test on enum type `{}`" ,
345+ struct_env. get_full_name_str( ) ,
346+ )
347+ } ;
348+ check_for_access_error_or_warning (
349+ env,
350+ fun_env,
351+ id,
352+ "tested" ,
353+ msg_maker,
354+ & struct_env. module_env ,
355+ * mid != caller_module_id,
356+ caller_is_inline_non_private,
357+ ) ;
358+ } ,
359+ Operation :: Pack ( mid, sid, _) => {
360+ let qualified_struct_id = mid. qualified ( * sid) ;
361+ let struct_env = env. get_struct ( qualified_struct_id) ;
377362 let msg_maker =
378- || format ! ( "unpack of `{}`" , struct_env. get_full_name_str( ) , ) ;
363+ || format ! ( "pack of `{}`" , struct_env. get_full_name_str( ) ) ;
379364 check_for_access_error_or_warning (
380365 env,
381366 fun_env,
382367 id,
383- "unpacked" ,
368+ "packed" ,
369+ msg_maker,
370+ & struct_env. module_env ,
371+ * mid != caller_module_id,
372+ caller_is_inline_non_private,
373+ ) ;
374+ } ,
375+ _ => {
376+ // all the other operations are either:
377+ // - not related to structs
378+ // - spec-only
379+ } ,
380+ } ,
381+ ExpData :: Assign ( _, pat, _)
382+ | ExpData :: Block ( _, pat, _, _)
383+ | ExpData :: Lambda ( _, pat, _, _, _) => {
384+ pat. visit_pre_post ( & mut |_, pat| {
385+ if let Pattern :: Struct ( id, str, _, _) = pat {
386+ let module_id = str. module_id ;
387+ let struct_env = env. get_struct ( str. to_qualified_id ( ) ) ;
388+ let msg_maker =
389+ || format ! ( "unpack of `{}`" , struct_env. get_full_name_str( ) , ) ;
390+ check_for_access_error_or_warning (
391+ env,
392+ fun_env,
393+ id,
394+ "unpacked" ,
395+ msg_maker,
396+ & struct_env. module_env ,
397+ module_id != caller_module_id,
398+ caller_is_inline_non_private,
399+ ) ;
400+ }
401+ } ) ;
402+ } ,
403+ ExpData :: Match ( _, discriminator, _) => {
404+ let discriminator_node_id = discriminator. node_id ( ) ;
405+ if let Type :: Struct ( mid, sid, _) =
406+ env. get_node_type ( discriminator_node_id) . drop_reference ( )
407+ {
408+ let qualified_struct_id = mid. qualified ( sid) ;
409+ let struct_env = env. get_struct ( qualified_struct_id) ;
410+ let msg_maker = || {
411+ format ! ( "match on enum type `{}`" , struct_env. get_full_name_str( ) , )
412+ } ;
413+ check_for_access_error_or_warning (
414+ env,
415+ fun_env,
416+ & discriminator_node_id,
417+ "matched" ,
384418 msg_maker,
385419 & struct_env. module_env ,
386- module_id != caller_module_id,
420+ mid != caller_module_id,
387421 caller_is_inline_non_private,
388422 ) ;
389423 }
390- } ) ;
391- } ,
392- ExpData :: Match ( _, discriminator, _) => {
393- let discriminator_node_id = discriminator. node_id ( ) ;
394- if let Type :: Struct ( mid, sid, _) =
395- env. get_node_type ( discriminator_node_id) . drop_reference ( )
396- {
397- let qualified_struct_id = mid. qualified ( sid) ;
398- let struct_env = env. get_struct ( qualified_struct_id) ;
399- let msg_maker =
400- || format ! ( "match on enum type `{}`" , struct_env. get_full_name_str( ) , ) ;
401- check_for_access_error_or_warning (
402- env,
403- fun_env,
404- & discriminator_node_id,
405- "matched" ,
406- msg_maker,
407- & struct_env. module_env ,
408- mid != caller_module_id,
409- caller_is_inline_non_private,
410- ) ;
411- }
412- } ,
413- ExpData :: Invalid ( _)
414- | ExpData :: Value ( ..)
415- | ExpData :: LocalVar ( ..)
416- | ExpData :: Temporary ( ..)
417- | ExpData :: Invoke ( ..)
418- | ExpData :: Quant ( ..)
419- | ExpData :: IfElse ( ..)
420- | ExpData :: Return ( ..)
421- | ExpData :: Sequence ( ..)
422- | ExpData :: Loop ( ..)
423- | ExpData :: LoopCont ( ..)
424- | ExpData :: Mutate ( ..) => { } ,
425- // access in specs is not restricted
426- ExpData :: SpecBlock ( _, _) => {
427- return false ;
428- } ,
424+ } ,
425+ ExpData :: Invalid ( _)
426+ | ExpData :: Value ( ..)
427+ | ExpData :: LocalVar ( ..)
428+ | ExpData :: Temporary ( ..)
429+ | ExpData :: Invoke ( ..)
430+ | ExpData :: Quant ( ..)
431+ | ExpData :: IfElse ( ..)
432+ | ExpData :: Return ( ..)
433+ | ExpData :: Sequence ( ..)
434+ | ExpData :: Loop ( ..)
435+ | ExpData :: LoopCont ( ..)
436+ | ExpData :: Mutate ( ..) => { } ,
437+ ExpData :: SpecBlock ( _, _) => {
438+ unreachable ! ( "we have already checked for spec blocks" ) ;
439+ } ,
440+ }
441+ } else {
442+ // post visit
443+ if matches ! ( exp, ExpData :: SpecBlock ( ..) ) {
444+ debug_assert ! ( spec_blocks_seen > 0 , "should match in pre and post" ) ;
445+ spec_blocks_seen -= 1 ;
446+ }
429447 }
430448 true
431449 } ) ;
0 commit comments