008240612s2023      us  |||||||||||||||c||eng  d
■001000016935240
■00520240214101909
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798380722575
■035    ▼a(MiAaPQ)AAI30685544
■035    ▼a(MiAaPQ)Purdue23750805
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a005
■1001  ▼aWei,  Guannan.
■24510▼aMetaprogramming  Program  Analyzers▼h[electronic  resource]
■260    ▼a[S.l.]:▼bPurdue  University.  ▼c2023
■260  1▼aAnn  Arbor  :▼bProQuest  Dissertations  &  Theses,  ▼c2023
■300    ▼a1  online  resource(307  p.)
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  85-05,  Section:  A.
■500    ▼aAdvisor:  Rompf,  Tiark.
■5021  ▼aThesis  (Ph.D.)--Purdue  University,  2023.
■506    ▼aThis  item  must  not  be  sold  to  any  third  party  vendors.
■520    ▼aStatic  program  analyzers  are  vital  tools  to  produce  useful  insights  about  programs  without  executing  these  programs.  These  insights  can  be  used  to  improve  the  quality  of  programs,  e.g.,  detecting  defects  in  programs,  or  optimizing  programs  to  use  fewer  resources.  However,  building  static  program  analyzers  that  are  simultaneously  sound,  performant,  and  flexible  is  notoriously  challenging.This  dissertation  aims  to  address  this  challenge  by  exploring  the  potential  of  applying  correct-by-construction  metaprogramming  techniques  to  build  static  program  analyzers.  Metaprogramming  techniques  manipulate  and  transform  programs  as  data  objects.  In  this  thesis,  we  consider  static  program  analyzers  as  the  objects  to  be  manipulated  or  transformed.  We  show  that  metaprogramming  techniques  can  improve  our  understanding,  the  construction,  flexibility,  and  performance  of  program  analyzers.We  first  study  the  inter-derivation  of  abstract  interpreters.  Using  off-the-shelf  program  transformation  techniques  such  as  refunctionalization,  we  demonstrate  that  big-step  abstract  interpreters  can  be  mechanically  derived  from  their  small-step  counterparts,  thus  building  a  functional  correspondence  between  two  different  styles  of  abstract  interpretation.To  build  high-performance  program  analyzers,  we  exploit  the  first  Futamura  projection  to  build  compilers  for  abstract  interpretation  and  symbolic  execution.  The  first  Futamura  projection  states  that  specializing  an  interpreter  with  respect  to  an  input  program  is  a  process  equivalent  to  compilation,  thus  providing  a  practical  way  to  repurpose  interpreters  for  compilation  and  code  generation.  We  systematically  apply  this  idea  to  build  programanalysis  compilers  by  writing  analyzers  as  staged  interpreters  using  higher-level  abstractions.  The  staged  interpreter  can  be  used  for  generating  sound  and  performant  analysis  code  given  a  specific  input  program.  Moreover,  the  approach  enables  using  abstractions  without  regret:  by  using  higher-level  program  abstractions,  the  analyzer  can  be  written  in  a  way  that  is  close  to  its  high-level  specification  (e.g.  big-step  operational  semantics),  and  by  compilation,  the  analyzer  is  performant  since  it  does  not  need  to  pay  the  runtime  overhead  of  using  these  abstraction  mechanisms.We  also  develop  novel  type  systems  that  track  sharing  and  separation  in  higher-order  imperative  languages.  Such  type  systems  are  useful  both  for  general-purpose  programming  languages  and  for  optimization  of  domain-specific  metaprograms  such  as  those  programanalysis  compilers.
■590    ▼aSchool  code:  0183.
■650  4▼aProgramming  languages.
■650  4▼aAlgebra.
■650  4▼aPerformance  evaluation.
■650  4▼aInterpreters.
■650  4▼aSemantics.
■650  4▼aComputer  science.
■650  4▼aLogic.
■650  4▼aTranslation  studies.
■690    ▼a0984
■690    ▼a0395
■690    ▼a0213
■71020▼aPurdue  University.
■7730  ▼tDissertations  Abstracts  International▼g85-05A.
■773    ▼tDissertation  Abstract  International
■790    ▼a0183
■791    ▼aPh.D.
■792    ▼a2023
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T16935240▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.
■980    ▼a202402▼f2024